[isabelle-dev] NEWS: more support for other ML applications

[Makarius]

*** ML ***

* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").

* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for Isabelle/ML, or "SML" for official Standard ML. It is also possible
to move toplevel bindings between environments, using a notation with
">" as separator. For example:

  declare [[ML_environment = "Isabelle>SML"]]
  ML ‹val println = writeln›

  declare [[ML_environment = "SML"]]
  ML ‹println "test"›

  declare [[ML_environment = "Isabelle"]]
  ML ‹println›  ― ‹not present›

The Isabelle/ML function ML_Env.setup defines new ML environments. This
is useful to incorporate big SML projects in an isolated name space, and
potentially with variations on ML syntax (existing ML_Env.SML_operations
observes the official standard).


This refers to Isabelle/7414ce0256e1.

It is the current state of various ongoing discussions about
incorporating other ML applications into the Isabelle environment (e.g.
OpenTheory, Metis, MetiTarski HOL4, ProofPower). There are two
motivations for this:

  (1) Developing these tools in the Isabelle Prover IDE
      (instead of vi or Emacs)

  (2) Using these tools inside Isabelle

A bit more work is required to make this really work in practice, but
this is an important stepping stone towards routine use of "ML
virtualization" (Isabelle can load Isabelle/Pure into itself, so it
should be able to load less complex applications, too).


	Makarius