On Wed, 3 Dec 2014, David Matthews wrote:
It all works by having the Poly/ML compiler as a function which takes a large set of parameters most of which have simple defaults. All the interaction with the compiler is through ML functions. The default REPL just calls the compiler with streams connected to the console but it's very easy for a user to replace the REPL with something else.
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.)
Makarius
---------------------------------------------------------------------------- http://stop-ttip.org 997,299 people so far ----------------------------------------------------------------------------