[isabelle-dev] NEWS: command 'ML_export'

[Makarius]

*** ML ***

* Command 'ML_export' exports ML toplevel bindings to the global
bootstrap environment of the ML process. This allows ML evaluation
without a formal theory context, e.g. in command-line tools like
"isabelle process".


This refers to Isabelle/cbee43ff4ceb.

Here are also the examples from the "system" manual in
Isabelle/b5d0318757f0:

  isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'
  isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'

In other words, it is now quite easy to produce clean command-line
tools, based on ML functions inside a regular Isabelle session.


	Makarius