theory

global imports finally honoured !

Now, this is a great day! SLuMB, the OMDoc file storage for ActiveMath supports <imports from="x" type="global"/>. This was a standard feature of OMDoc specification but was never supported. I finally understood that this is the clean-way to support the management of big files and I even successfully split a LeAM_calculus monster-file in two without breaking references.

Chapter 6: reference management

Reference is the general word used to describe a relation between a location in OMDoc documents to another. Sometimes the word dependency is also used although this is old.

References generally point to an element that has an id attribute (therefore it’s useful for you to put good ids that you will remember). An element with id myId within a theory element of id myTheoryId, all within a collection of identifier collectionId can be referenced as follows:

  • within the same theory element it is in, using simply myId
  • from another theory of the same collection, it can be
Syndicate content