[isabelle-dev] NEWS: process management (summary and update)

[Makarius]

*** System ***

* The Isabelle system environment always ensures that the main
executables are found within the shell search $PATH: "isabelle" and
"isabelle_scala_script".

* The Isabelle ML process is now managed directly by Isabelle/Scala, and
shell scripts merely provide optional command-line access. In
particular:

   . Scala module ML_Process to connect to the raw ML process,
     with interaction via stdin/stdout/stderr or in batch mode;
   . command-line tool "isabelle console" as interactive wrapper;
   . command-line tool "isabelle process" as batch mode wrapper.

* The executable "isabelle_process" has been discontinued. Tools and
prover front-ends should use ML_Process or Isabelle_Process in
Isabelle/Scala. INCOMPATIBILITY.

* New command-line tool "isabelle process" supports ML evaluation of
literal expressions (option -e) or files (option -f) in the context of a
given heap image. Errors lead to premature exit of the ML process with
return code 1.

* Command-line tool "isabelle console" provides option -r to help to
bootstrapping Isabelle/Pure interactively.

* File.bash_string, File.bash_path etc. represent Isabelle/ML and
Isabelle/Scala strings authentically within GNU bash. This is useful to
produce robust shell scripts under program control, without worrying
about spaces or special characters. Note that user output works via
Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
less versatile) operations File.shell_quote, File.shell_path etc. have
been discontinued.


This refers to Isabelle/cf79f8866bc3.

What is not written in the NEWS, because it is not directly user-relevant: 
the major Isabelle tools (build, process, console etc.) are all done in 
Isabelle/Scala. The outermost shell script calls more or less directly 
into some JVM class with its "main" method. The Bash getopts handling is 
imitated faithfully via the Getopts module in Isabelle/Scala.

All this significantly changes the way of Isabelle system programming. 
>From here we can take a new and fresh look at it, and think of further 
improvements later.


 	Makarius