Omar, I recently installed ProofPower http://www.lemma-one.com/ProofPower/index/index.htmland discovered that it has capabilities as an efficient and effective PolyML IDE too! It also uses a simplified variation of Knuth's "literate programming" idea where you can intersperse mathematics with the correct symbols (rather than ASCII code approximations). In an earlier post, I had mistakenly claimed that ProofPower required an earilier version of PolyML (v 4), but Rob Arthan helped me through the very minor update to a makefile to get it to build easily using the latest PolyML version, so that is not a problem. I have attached a small sample to show how the integration works with math using a few macros in the source code. The source (in the doc file) was entered using the xpp "IDE" which allows you to run the SML code right in the editor. -Dave Topham

2. Re: [isabelle] Isabelle as an SML environment and IDE (Omar Montano Rivas)

---

Date: Mon, 22 Dec 2014 11:50:28 -0600 From: Omar Montano Rivas <omarmrivas at gmail.com> To: Aleks Kissinger <aleks0 at gmail.com> Cc: isabelle-users at cl.cam.ac.uk, Poly/ML Mailing List <polyml at inf.ed.ac.uk> Subject: Re: [isabelle] Isabelle as an SML environment and IDE

Really useful. Thanks for sharing.

Best, Omar.

2014-12-19 10:49 GMT-06:00 Aleks Kissinger <aleks0 at gmail.com>:

...

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_en...

...

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"