NEWS: Isabelle_System.ML_process vs. "isabelle ML_process"

[Makarius]

*** ML ***

* Isabelle_System.ML_process and ML_Process.args allow to run an
external ML process directly via the current Isabelle/Scala context,
without running another bulky Java process of "isabelle ML_process" on
the command-line.


*** System ***

* The former command-line tool "isabelle process" has been renamed to
"isabelle ML_process", with new options -C DIR and -r (redirect). The
old option option -T to load individual theories via the Isabelle/ML
"use_thy" function has been removed. It is still possible to use
"Thy_Info.use_thy_legacy" together with "isabelle ML_process -e ...",
but that low-level entry to the theory loader will be removed at a later
stage. The proper way to process individual theories under program
control is via "isabelle process_theories". INCOMPATIBILITY.


This refers to Isabelle/baf75b1bf14a.

It is a clarification of ancient terminology and concepts. Many decades ago, 
an "Isabelle process" was indeed the Poly/ML runtime system with our modest 
Pure/ROOT.ML or HOL/ROOT.ML pre-loaded. In the past 10 years, the "Isabelle 
system process" has become a Java Virtual Machine running the bulky 
isabelle.jar (11 MiB of JVM byte code). That Isabelle system process can start 
any number of Isabelle/ML processes, using operations from the Scala modules 
isabelle.ML_Process and isabelle.Bash. Isabelle/ML programs can now directly 
invoke that as well, e.g. to run a generated SML program via Isabelle/HOL codegen.

So ML-to-ML_process now goes via the already running Scala process, and not 
ML-to-Bash.Server-to-java_process-to-ML_process.

To see the wiring, it might help to use the Prover IDE:

    isabelle jedit -l Pure ~/Scratch.thy src/Pure/ROOT.ML

and then explore this source snippet via C-hover-click:

theory Scratch
   imports Pure
begin

ML ‹
   Isabelle_System.ML_process;
   \<^scala_function>‹ML_process›;
›

end


We don't have a proper Isabelle/Scala IDE yet: One happy day it will be part 
of the regular Isabelle/PIDE setup -- not the somewhat lacking IntelliJ IDEA 
Scala plugin.


	Makarius