--- 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
--- 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"
--- 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 $_;
}
-
--- 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:
--- 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