[isabelle-dev] NEWS: command 'ML_export'

Makarius makarius at sketis.net
Fri May 25 23:32:10 CEST 2018

*** 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 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.


More information about the isabelle-dev mailing list