On Thu, 11 Dec 2014, Peter Gammie wrote:
On 11 Dec 2014, at 4:14, Makarius <makarius at sketis.net> wrote:
I don?t "hack" on Isabelle/Pure, but edit it carefully and thoughtfully, using plain jEdit with its static ML mode.
Sounds like I might as well use emacs rather than ?plain jEdit with its static ML mode? for this purpose.
I did this myself until 2006 and then switched to jEdit. After 2 weeks of unlearning ESCAPE-META-ALT-CONTROL-SHIFT I became much more productive with the new editor. Then I set out to make a full-scale IDE based on it: 8 years later it is there.
It is still not possible to load this ML bootstrap environment of Isabelle into Isabelle/PIDE, though. There are some partial solutions to that: many ML modules of Isabelle/Pure can be loaded individually into the Prover IDE via ML_file in Pure.thy.
So, err, if my little project is more like the ?ML bootstrap environment of Isabelle? and less like ?many modules of Isabelle/Pure? then ?the Prover IDE? is not going to help me, is it?
As I said, the Prover IDE can load many modules of Isabelle/Pure later on, as a second copy within the context of Pure.thy. I still wonder how relevant this is for users of PIDE for general ML development, even for users of Isabelle. As a user of Linux I also don't edit the kernel sources, neither do I "hack" on it.
Below Pure.thy several delicate bootstrap stages turn the raw ML system into something that can then support user-space Isabelle/ML, and now also regular Standard ML.
So I think we run the risk of the no true Scotsman fallacy here. One could argue that Isabelle is not an SML program (ah, I note you said it was the ?largest ML program that I know of?).
Isabelle/Pure is definitely not an SML program. I usually say "ML" in a general sense, and "SML" in the specific sense of SML'97.
The "largest ML program that I know of" was referring to Isabelle/HOL: it is an application of Isabelle/ML with Pure.thy as starting point.
Makarius
---------------------------------------------------------------------------- http://stop-ttip.org 1,138,652 people so far ----------------------------------------------------------------------------