*** 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
