[isabelle-dev] Notes and updates on Isabelle/ML

[Makarius]

Here are some cumulative notes on Isabelle/ML wrt. current 
Isabelle/20cf88cd3188, about new and old things.

   * The configuration options ML_source_trace, ML_exception_trace,
     ML_print_depth control various aspects of ML compilation and run-time
     within the regular context -- as usual in a stateless manner.
     ML_exception_trace may be also configured in the global state of the
     session (via Isabelle/jEdit plugin options), since it is sometimes
     used outside of a context.

   * PolyML.makestring is very old-fashioned (and non-portable):
     @{make_string} of Isabelle/ML is the documented way to do one-shot
     output of ML values.  Such things are not meant to persist:  proper
     tools should produce proper error messages for proper users (which is
     considerable work to get right).  In contrast, internal failure is
     just emitted as internal exception, without any special printing --
     the ML toplevel does that already.

   * Isabelle/ML code must never ever handle arbitrary exceptions (as
     explained in the "implementation" manual).  The Isabelle/ML IDE now
     shows explicit warnings about these dreaded catch-all patterns, by
     enabling a flag that David Matthews had kindly provided some years
     ago.

   * pointer_eq is not part of SML and requires extra reasoning that it is
     correct whenever it is used (normally in certain hot-spots of kernel
     operations).  See also the surprise caused by some optimizations of
     the Poly/ML runtime system concerning object identity, which are
     perfectly inside the Standard ML semantics:
     http://lists.inf.ed.ac.uk/pipermail/polyml/2014-January/001389.html

Concerning the last point, I did not inspect the actual situation outside 
of Isabelle/Pure yet.  It probably requires further looking, and more 
explanations on either of the mailing lists.


 	Makarius