David, Makarius,
On 3 Dec 2014, at 13:20, Makarius <makarius at sketis.net> wrote:
Here is also an example for that, to implement a home-made "eval" function in Poly/ML: http://stackoverflow.com/questions/9555790/does-sml-poly-have-a-cl-like-repl
This should give some clues how to do it. It is up to that function to say how errors are printed.
An actual REPL requires a bit more work, with proper handling of interrupts in contrast to regular exceptions. Isabelle2014 still happens to have such a REPL in isar.ML, but it is not used by default and already deleted for the next release. (Such a nostalgic REPL is actually more complicated than having a direct editing model that is now standard in Isabelle/PIDE.)
Thanks for the pointer. I?ve stashed this one away for a rainy day. Right now I just want to interact with Poly/ML in the most straightforward way.
On 3 Dec 2014, at 5:33, David Matthews <dm at prolingua.co.uk> wrote:
It would be nice to have SML emacs mode working with Poly/ML for those who would like to use it but my feeling is that it is rather old-fashioned. Poly/ML now supports a much more extensive interface designed for an IDE. The best example of this is Isabelle's ML mode. See http://sketis.net/2014/isabellepide-as-ide-for-standard-ml which has a nice screen-shot. Lucas Dixon and I both had a go at producing IDEs which were completely independent of Isabelle but we didn?t get as far as Makarius has.
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?
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?)
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.
BTW I have no problem cranking out .thy files as a kind of fake build system if that?s what it takes.
The format that the default REPL uses for error messages was one that was used by various compilers at one time and it used to be possible to parse it automatically. If there's a more up-to-date format I'm happy to change to it. I don?t know if anyone is parsing the current format automatically and would be inconvenienced by a change.
Me neither. Hide it under a flag? Or are you (and Makarius) suggesting that I hand-roll my own REPL? (I?m not adverse to that either.)
thanks, peter