Really useful. Thanks for sharing. Best, Omar.
2014-12-19 10:49 GMT-06:00 Aleks Kissinger <[email protected]>: > It recently came up on the Poly/ML mailing list that Isabelle/jEdit > makes a pretty efficient SML IDE these days. I manage a fairly large > SML project called Quantomatic, so I thought I'd have a go at getting > a setup to work. I've got a setup now that I am pretty happy with, so > I thought I'd share my results. Hopefully other people will find this > helpful. > > Quantomatic is fairly unique in that it is designed to run inside of > Isabelle or as a standalone project. As a result, the whole codebase > is implemented on top of an Isabelle/ML-like environment, obtained by > importing chunks of the ML code in Pure. This can be done by copying > src/Pure from Isabelle 2014 into an SML project and using this file: > > > https://github.com/Quantomatic/quantomatic/blob/integration/core/isabelle_env.ML > > In the past, we used a slightly hacked-up version of Pure, but for the > sake of maintainability, we now use an exact copy. > > The project itself is loaded with special "thy" files that only > contain comments and "ML_file" commands. These can be run from inside > Isabelle/jEdit (in the "real" Isabelle/ML environment), or they can be > imported in poly/ML with the function "use_thy": > > https://github.com/Quantomatic/quantomatic/blob/integration/core/use_thy.ML > > This implements a baby version of the outer syntax parser, which > ignores imports and translates the ML_file commands into use > statements. This makes the external ROOT.ML tiny and easy to maintain: > > https://github.com/Quantomatic/quantomatic/blob/integration/core/ROOT.ML > > This can be executed with, e.g. "poly --use ROOT.ML" > >
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
