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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
