On Wed, 10 Dec 2014, Peter Gammie wrote:
I?m not adverse to trying out JEdit, but it seems to dodge the issues somewhat. Is anyone using it for hacking large-scale SML programs?
The largest ML program that I know of is Isabelle/HOL with all its add-on tools: even big things like the Metis prover are incorporated there. The Prover IDE is used routinely for editing Isabelle/HOL theories and ML modules -- I also made special tricks in IDE memory management to support this on current mainstream/low-end hardware with only 8 GB.
One measure of adequacy might be if JEdit/SML (err, Isabelle/SML?) can load the foundational Isabelle stuff, e.g. Pure/ROOT.ML. (How do you hack Isabelle/Pure presently?)
I don't "hack" on Isabelle/Pure, but edit it carefully and thoughtfully, using plain jEdit with its static ML mode. 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.
In particular I?d want access to Poly/ML?s concurrency primitives. It seems to nuke Poly/ML?s ?use? function, which is a little unfriendly.
Can you explain what you mean? PolyML.use is not part of the SML standard. The Isabelle/SML environment takes care to load sources via 'SML_file' commands -- it has to do that to manage changes and versions properly.
BTW I have no problem cranking out .thy files as a kind of fake build system if that?s what it takes.
This sounds like you still think in terms of "make" files to build things. In PIDE you just assemble your project, presently by some .thy file as shown in the SML example in the Documentation panel, and then edit without further thinking about it.
An open problem is to generate a compiled application directly from this IDE model, but right now Isabelle/SML is not a specific "product" for such standalone application development yet (unless you want to ship it as Isabelle session).
Makarius
---------------------------------------------------------------------------- http://stop-ttip.org 1,127,322 people so far ----------------------------------------------------------------------------