# HG changeset patch
# User wenzelm
# Date 1457037031 -3600
# Node ID 860cd901ab43267fa6028b0f7481a09898657c26
# Parent  9e2a65912111812025a9fe7f737e09526598db81
clarified isabelle_process;

diff -r 9e2a65912111 -r 860cd901ab43 NEWS
--- a/NEWS	Thu Mar 03 15:23:02 2016 +0100
+++ b/NEWS	Thu Mar 03 21:30:31 2016 +0100
@@ -998,6 +998,10 @@
 
 *** System ***
 
+* Command-line tool "isabelle_process" supports ML evaluation of literal
+expressions (option -e) or files (option -f). Errors lead to premature
+exit of the ML process with return code 1.
+
 * Command-line tool "isabelle console" enables print mode "ASCII".
 
 * Command-line tool "isabelle update_then" expands old Isar command
diff -r 9e2a65912111 -r 860cd901ab43 bin/isabelle_process
--- a/bin/isabelle_process	Thu Mar 03 15:23:02 2016 +0100
+++ b/bin/isabelle_process	Thu Mar 03 21:30:31 2016 +0100
@@ -29,7 +29,8 @@
   echo "    -O           system options from given YXML file"
   echo "    -P SOCKET    startup process wrapper via TCP socket"
   echo "    -S           secure mode -- disallow critical operations"
-  echo "    -e ML_TEXT   pass ML_TEXT to the ML session"
+  echo "    -e ML_EXPR   evaluate ML expression on startup"
+  echo "    -f ML_FILE   evaluate ML file on startup"
   echo "    -m MODE      add print mode for output"
   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -q           non-interactive session"
@@ -47,6 +48,11 @@
   exit 2
 }
 
+function check_file()
+{
+  [ ! -f "$1" ] && fail "Bad file: \"$1\""
+}
+
 
 ## process command line
 
@@ -55,12 +61,12 @@
 OPTIONS_FILE=""
 PROCESS_SOCKET=""
 SECURE=""
-ML_TEXT=""
+declare -a LAST_ML_OPTIONS=()
 MODES=""
 declare -a SYSTEM_OPTIONS=()
 TERMINATE=""
 
-while getopts "O:P:Se:m:o:q" OPT
+while getopts "O:P:Se:f:m:o:q" OPT
 do
   case "$OPT" in
     O)
@@ -73,7 +79,12 @@
       SECURE=true
       ;;
     e)
-      ML_TEXT="$ML_TEXT $OPTARG"
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
+      ;;
+    f)
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use"
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
       ;;
     m)
       if [ -z "$MODES" ]; then
@@ -116,6 +127,8 @@
 
 ## heap file
 
+declare -a FIRST_ML_OPTIONS=()
+
 [ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC"
 
 case "$HEAP" in
@@ -146,6 +159,31 @@
     ;;
 esac
 
+if [ -z "$HEAP_FILE" ]; then
+  case "$ML_PLATFORM" in
+    *-windows)
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
+      ;;
+    *)
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
+      ;;
+  esac
+else
+  check_file "$HEAP_FILE"
+  case "$ML_PLATFORM" in
+    *-windows)
+      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
+      ;;
+    *)
+      PLATFORM_HEAP_FILE="$HEAP_FILE"
+      ;;
+  esac
+  PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")"
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success)"
+fi
 
 
 ## prepare tmp directory
@@ -157,16 +195,21 @@
 chmod $(umask -S) "$ISABELLE_TMP"
 
 
-## run it!
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+## ML text
 
-[ -n "$MODES" ] && ML_TEXT="Unsynchronized.change print_mode (append [$MODES]); $ML_TEXT"
+if [ -n "$MODES" ]; then
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Unsynchronized.change print_mode (append [$MODES])"
+fi
 
-[ -n "$SECURE" ] && ML_TEXT="$ML_TEXT; Secure.set_secure ();"
+if [ -n "$SECURE" ]; then
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()"
+fi
 
 if [ -n "$PROCESS_SOCKET" ]; then
-  ML_TEXT="$ML_TEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Isabelle_Process.init \"$PROCESS_SOCKET\""
 else
   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   if [ -n "$OPTIONS_FILE" ]; then
@@ -179,18 +222,33 @@
       fail "Failed to retrieve Isabelle system options"
   fi
   if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then
-    ML_TEXT="Exn.capture_exit 2 Options.load_default (); $ML_TEXT"
+    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()"
   fi
 fi
 
-export HEAP_FILE ML_TEXT TERMINATE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
+
+## ML process
+
+check_file "$ML_HOME/poly"
+librarypath "$ML_HOME"
+
+export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
 
-if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
-  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+if [ -n "$TERMINATE" ]; then
+  "$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \
+    "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" </dev/null
+  RC="$?"
 else
-  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+  "$ISABELLE_HOME/lib/scripts/feeder" -p | \
+    {
+      read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}"
+      RC="$?"
+      kill -TERM "$FPID"
+      exit "$RC"
+    }
+  RC="$?"
 fi
-RC="$?"
 
 [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
 rmdir "$ISABELLE_TMP"
diff -r 9e2a65912111 -r 860cd901ab43 lib/scripts/recode.pl
--- a/lib/scripts/recode.pl	Thu Mar 03 15:23:02 2016 +0100
+++ b/lib/scripts/recode.pl	Thu Mar 03 21:30:31 2016 +0100
@@ -7,6 +7,5 @@
 for (@ARGV) {
   utf8::upgrade($_);
   s/([\x80-\xff])/\\${\(ord($1))}/g;
-  print $_, " ";
+  print $_;
 }
-
diff -r 9e2a65912111 -r 860cd901ab43 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Mar 03 15:23:02 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.6.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## heap file
-
-if [ -z "$HEAP_FILE" ]; then
-  case "$ML_PLATFORM" in
-    *-windows)
-      INIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
-      ;;
-    *)
-      INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-      ;;
-  esac
-else
-  check_file "$HEAP_FILE"
-  case "$ML_PLATFORM" in
-    *-windows)
-      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
-      ;;
-    *)
-      PLATFORM_HEAP_FILE="$HEAP_FILE"
-      ;;
-  esac
-  INIT="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success);"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -n "$TERMINATE" ]; then
-  "$ML_HOME/poly" -q -i $ML_OPTIONS \
-    --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$ML_TEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" | \
-    { read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r 9e2a65912111 -r 860cd901ab43 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Thu Mar 03 15:23:02 2016 +0100
+++ b/src/Doc/System/Basics.thy	Thu Mar 03 21:30:31 2016 +0100
@@ -300,7 +300,8 @@
     -O           system options from given YXML file
     -P SOCKET    startup process wrapper via TCP socket
     -S           secure mode -- disallow critical operations
-    -e ML_TEXT   pass ML_TEXT to the ML session
+    -e ML_EXPR   evaluate ML expression on startup
+    -f ML_FILE   evaluate ML file on startup
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -q           non-interactive session
@@ -323,10 +324,10 @@
 subsubsection \<open>Options\<close>
 
 text \<open>
-  Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be passed to the Isabelle
-  session from the command line. Multiple \<^verbatim>\<open>-e\<close> options are evaluated in the
-  given order. Strange things may happen when erroneous ML code is provided.
-  Also make sure that the ML commands are terminated properly by semicolon.
+  Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
+  started. The source is either given literally or taken from a file. Multiple
+  \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
+  premature exit of the ML process with return code 1.
 
   \<^medskip>
   The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this