# HG changeset patch
# User wenzelm
# Date 1457644861 -3600
# Node ID 98122e719d1928e6478a99946d1185cd375aa887
# Parent  0c837beeb5e778aecdc586c2e2e06624050203a5
tuned;

diff -r 0c837beeb5e7 -r 98122e719d19 NEWS
--- a/NEWS	Thu Mar 10 22:09:44 2016 +0100
+++ b/NEWS	Thu Mar 10 22:21:01 2016 +0100
@@ -218,16 +218,22 @@
 
 *** System ***
 
-* SML/NJ and old versions of Poly/ML are no longer supported.
+* 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. Command-line usage works via "isabelle process" or
-"isabelle console". INCOMPATIBILITY.
-
-* The Isabelle system environment always ensures that the main
-executables are found within the shell search $PATH: "isabelle" and
-"isabelle_scala_script".
+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
@@ -249,6 +255,8 @@
 less versatile) operations File.shell_quote, File.shell_path etc. have
 been discontinued.
 
+* SML/NJ and old versions of Poly/ML are no longer supported.
+
 
 
 New in Isabelle2016 (February 2016)