On Thu, 11 Dec 2014, Peter Gammie wrote:
On 11 Dec 2014, at 4:14, Makarius <makar...@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
----------------------------------------------------------------------------_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
