UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

Persist results of diagram operators to OMDoc #566

Open ComFreek opened 2 years ago

ComFreek commented 2 years ago

Currently, modules resulting from diagram operators are not persisted to OMDoc. This means that in every new MMT session all usages of diagram structural features need to be re-typechecked and re-elaborated. This is especially daunting when working with multiple files, as is the case in LATIN.

If such modules are persisted, then we should also persist the resulting diagrams (of module paths) that are currently stored into diag.dfC.normalized (where diag is a module instance of the diagram structural feature). In particular, say if file1 contains diagram diag : ?meta = diagexpr... and file1 is built, then in any subsequent (possibly new) MMT session, file2 should be able to reference not only the modules that were built by diag but also able to reference diag itself (i.e., diag.dfC.normalized containing exactly what was written when building file1).

PS: This is out-of-scope for my thesis, hence something for future work by somebody else.