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
----------------------------------------------------------------------------
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
