--- a/NEWS Mon Feb 29 16:35:15 2016 +0100
+++ b/NEWS Mon Feb 29 20:43:16 2016 +0100
@@ -185,6 +185,11 @@
executables are found within the PATH: isabelle, isabelle_process,
isabelle_scala_script.
+* The isabelle_process executable no longer supports writable heap
+images. INCOMPATIBILITY in exotic situations where "isabelle build"
+cannot be used: the structure ML_Heap provides operations to save the ML
+heap under program control.
+
* The somewhat pointless command-line tool "isabelle yxml" has been
discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
"YXML" in Isabelle/ML or Isabelle/Scala.
--- a/bin/isabelle_process Mon Feb 29 16:35:15 2016 +0100
+++ b/bin/isabelle_process Mon Feb 29 20:43:16 2016 +0100
@@ -1,6 +1,6 @@
#!/usr/bin/env bash
#
-# Author: Markus Wenzel, TU Muenchen
+# Author: Makarius
#
# Isabelle process startup script.
@@ -23,23 +23,20 @@
function usage()
{
echo
- echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
+ echo "Usage: $PRG [OPTIONS] [HEAP]"
echo
echo " Options are:"
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 MLTEXT pass MLTEXT to the ML session"
+ echo " -e ML_TEXT pass ML_TEXT to the ML session"
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"
- echo " -r open heap file read-only"
- echo " -w reset write permissions on OUTPUT"
echo
- echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
- echo " These are either names to be searched in the Isabelle path, or"
- echo " actual file names (containing at least one /)."
- echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
+ echo " If HEAP is a plain name (default \"$ISABELLE_LOGIC\"), it is searched in \$ISABELLE_PATH;"
+ echo " if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,"
+ echo " the initial ML heap is used."
echo
exit 1
}
@@ -58,14 +55,12 @@
OPTIONS_FILE=""
PROCESS_SOCKET=""
SECURE=""
-MLTEXT=""
+ML_TEXT=""
MODES=""
declare -a SYSTEM_OPTIONS=()
TERMINATE=""
-READONLY=""
-NOWRITE=""
-while getopts "O:P:Se:m:o:qrw" OPT
+while getopts "O:P:Se:m:o:q" OPT
do
case "$OPT" in
O)
@@ -78,7 +73,7 @@
SECURE=true
;;
e)
- MLTEXT="$MLTEXT $OPTARG"
+ ML_TEXT="$ML_TEXT $OPTARG"
;;
m)
if [ -z "$MODES" ]; then
@@ -93,12 +88,6 @@
q)
TERMINATE=true
;;
- r)
- READONLY=true
- ;;
- w)
- NOWRITE=true
- ;;
\?)
usage
;;
@@ -110,16 +99,10 @@
# args
-INPUT=""
-OUTPUT=""
+HEAP=""
if [ "$#" -ge 1 ]; then
- INPUT="$1"
- shift
-fi
-
-if [ "$#" -ge 1 ]; then
- OUTPUT="$1"
+ HEAP="$1"
shift
fi
@@ -131,20 +114,20 @@
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
-## input heap file
+## heap file
-[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
+[ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC"
-case "$INPUT" in
+case "$HEAP" in
RAW_ML_SYSTEM)
- INFILE=""
+ HEAP_FILE=""
;;
*/*)
- INFILE="$INPUT"
- [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
+ HEAP_FILE="$HEAP"
+ [ ! -f "$HEAP_FILE" ] && fail "Bad heap file: \"$HEAP_FILE\""
;;
*)
- INFILE=""
+ HEAP_FILE=""
ISA_PATH=""
splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
@@ -152,11 +135,11 @@
do
DIR="$DIR/$ML_IDENTIFIER"
ISA_PATH="$ISA_PATH $DIR\n"
- [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
+ [ -z "$HEAP_FILE" -a -f "$DIR/$HEAP" ] && HEAP_FILE="$DIR/$HEAP"
done
- if [ -z "$INFILE" ]; then
- echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
+ if [ -z "$HEAP_FILE" ]; then
+ echo "Unknown logic \"$HEAP\" -- no heap file found in:" >&2
echo -ne "$ISA_PATH" >&2
exit 2
fi
@@ -164,24 +147,6 @@
esac
-## output heap file
-
-case "$OUTPUT" in
- "")
- if [ -z "$READONLY" -a -w "$INFILE" ]; then
- perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
- fi
- ;;
- */*)
- OUTFILE="$OUTPUT"
- ;;
- *)
- mkdir -p "$ISABELLE_OUTPUT"
- chmod $(umask -S) "$ISABELLE_OUTPUT"
- OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
- ;;
-esac
-
## prepare tmp directory
@@ -196,12 +161,12 @@
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
+[ -n "$MODES" ] && ML_TEXT="Unsynchronized.change print_mode (append [$MODES]); $ML_TEXT"
-[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
+[ -n "$SECURE" ] && ML_TEXT="$ML_TEXT; Secure.set_secure ();"
if [ -n "$PROCESS_SOCKET" ]; then
- MLTEXT="$MLTEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
+ ML_TEXT="$ML_TEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
else
ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
if [ -n "$OPTIONS_FILE" ]; then
@@ -213,12 +178,12 @@
"$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
fail "Failed to retrieve Isabelle system options"
fi
- if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
- MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
+ if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then
+ ML_TEXT="Exn.capture_exit 2 Options.load_default (); $ML_TEXT"
fi
fi
-export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
+export HEAP_FILE ML_TEXT TERMINATE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
"$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
--- a/lib/scripts/run-polyml Mon Feb 29 16:35:15 2016 +0100
+++ b/lib/scripts/run-polyml Mon Feb 29 20:43:16 2016 +0100
@@ -5,7 +5,7 @@
#
# Startup script for Poly/ML 5.6.
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+export -n HEAP_FILE ML_TEXT TERMINATE
## diagnostics
@@ -16,91 +16,55 @@
exit 2
}
-function fail_out()
-{
- fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
function check_file()
{
[ ! -f "$1" ] && fail "Unable to locate \"$1\""
}
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
+## heap file
-case "$ML_PLATFORM" in
- *-windows)
- PLATFORM_INFILE="$(platform_path -m "$INFILE")"
- PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
- ;;
- *)
- PLATFORM_INFILE="$INFILE"
- PLATFORM_OUTFILE="$OUTFILE"
- ;;
-esac
-
-if [ -z "$INFILE" ]; then
- INIT=""
+if [ -z "$HEAP_FILE" ]; then
case "$ML_PLATFORM" in
*-windows)
- EXIT="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 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));"
;;
*)
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+ INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
;;
esac
else
- check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
- EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
- MLEXIT=""
-else
- if [ -z "$INFILE" ]; then
- MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
- else
- MLEXIT="Session.save \"$OUTFILE\";"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+ check_file "$HEAP_FILE"
+ case "$ML_PLATFORM" in
+ *-windows)
+ PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
+ ;;
+ *)
+ PLATFORM_HEAP_FILE="$HEAP_FILE"
+ ;;
+ esac
+ INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); 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
-## run it!
+## poly process
+
+ML_TEXT="$INIT $ML_TEXT"
-MLTEXT="$INIT $EXIT $MLTEXT"
+check_file "$ML_HOME/poly"
+librarypath "$ML_HOME"
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
- "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+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
- if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
- else
- FEEDER_OPTS="-q"
- ML_OPTIONS="$ML_OPTIONS --error-exit"
- fi
- "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+ "$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
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
exit "$RC"
#:wrap=soft:maxLineLen=100:
--- a/lib/scripts/run-polyml-5.3.0 Mon Feb 29 16:35:15 2016 +0100
+++ b/lib/scripts/run-polyml-5.3.0 Mon Feb 29 20:43:16 2016 +0100
@@ -4,7 +4,7 @@
#
# Startup script for Poly/ML 5.3.0.
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+export -n HEAP_FILE ML_TEXT TERMINATE
## diagnostics
@@ -15,54 +15,28 @@
exit 2
}
-function fail_out()
-{
- fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
function check_file()
{
[ ! -f "$1" ] && fail "Unable to locate \"$1\""
}
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
## prepare databases
-if [ -z "$INFILE" ]; then
- INIT=""
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+if [ -z "$HEAP_FILE" ]; then
+ INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
else
- check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
- EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
- MLEXIT=""
-else
- if [ -z "$INFILE" ]; then
- MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
- else
- MLEXIT="Session.save \"$OUTFILE\";"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+ check_file "$HEAP_FILE"
+ INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
fi
-## run it!
+## poly process
-MLTEXT="$INIT $EXIT $MLTEXT"
+ML_TEXT="$INIT $ML_TEXT"
+
+check_file "$ML_HOME/poly"
+librarypath "$ML_HOME"
if [ -z "$TERMINATE" ]; then
FEEDER_OPTS=""
@@ -70,12 +44,10 @@
FEEDER_OPTS="-q"
fi
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
+ { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
RC="$?"
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
exit "$RC"
#:wrap=soft:maxLineLen=100:
--- a/src/Doc/System/Basics.thy Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Doc/System/Basics.thy Mon Feb 29 20:43:16 2016 +0100
@@ -291,28 +291,25 @@
text \<open>
The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle
logic sessions --- either interactively or in batch mode. It provides an
- abstraction over the underlying ML system, and over the actual heap file
- locations. Its usage is:
+ abstraction over the underlying ML system and its saved heap files. Its
+ usage is:
@{verbatim [display]
-\<open>Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
+\<open>Usage: isabelle_process [OPTIONS] [HEAP]
Options are:
-O system options from given YXML file
-P SOCKET startup process wrapper via TCP socket
-S secure mode -- disallow critical operations
- -e MLTEXT pass MLTEXT to the ML session
+ -e ML_TEXT pass ML_TEXT to the ML session
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-q non-interactive session
- -r open heap file read-only
- -w reset write permissions on OUTPUT
- INPUT (default "$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
- These are either names to be searched in the Isabelle path, or
- actual file names (containing at least one /).
- If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.\<close>}
+ If HEAP is a plain name (default "HOL"), it is searched in $ISABELLE_PATH;
+ if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,
+ the initial ML heap is used.\<close>}
- Input files without path specifications are looked up in the @{setting
+ Heap files without path specifications are looked up in the @{setting
ISABELLE_PATH} setting, which may consist of multiple components separated
by colons --- these are tried in the given order with the value of @{setting
ML_IDENTIFIER} appended internally. In a similar way, base names are
@@ -326,24 +323,6 @@
subsubsection \<open>Options\<close>
text \<open>
- If the input heap file does not have write permission bits set, or the \<^verbatim>\<open>-r\<close>
- option is given explicitly, then the session started will be read-only. That
- is, the ML world cannot be committed back into the image file. Otherwise, a
- writable session enables commits into either the input file, or into another
- output heap file (if that is given as the second argument on the command
- line).
-
- The read-write state of sessions is determined at startup only, it cannot be
- changed intermediately. Also note that heap images may require considerable
- amounts of disk space (hundreds of MB or some GB). Users are responsible for
- themselves to dispose their heap files when they are no longer needed.
-
- \<^medskip>
- The \<^verbatim>\<open>-w\<close> option makes the output heap file read-only after terminating.
- Thus subsequent invocations cause the logic image to be read-only
- automatically.
-
- \<^medskip>
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.
@@ -385,30 +364,14 @@
@{setting ISABELLE_LOGIC} setting) like this:
@{verbatim [display] \<open>isabelle_process\<close>}
- Usually @{setting ISABELLE_LOGIC} refers to one of the standard logic
- images, which are read-only by default. A writable session --- based on
- \<^verbatim>\<open>HOL\<close>, but output to \<^verbatim>\<open>Test\<close> (in the directory specified by the @{setting
- ISABELLE_OUTPUT} setting) --- may be invoked as follows:
- @{verbatim [display] \<open>isabelle_process HOL Test\<close>}
-
- Ending this session normally (e.g.\ by typing control-D) dumps the whole ML
- system state into \<^verbatim>\<open>Test\<close> (be prepared for more than 100\,MB):
-
- The \<^verbatim>\<open>Test\<close> session may be continued later (still in writable state) by:
- @{verbatim [display] \<open>isabelle_process Test\<close>}
-
- A read-only \<^verbatim>\<open>Test\<close> session may be started by:
- @{verbatim [display] \<open>isabelle_process -r Test\<close>}
-
- \<^bigskip>
+ \<^medskip>
The next example demonstrates batch execution of Isabelle. We retrieve the
\<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
quoting rules for the Bash shell vs.\ ML):
- @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL\<close>}
+ @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q HOL\<close>}
Note that the output text will be interspersed with additional junk messages
- by the ML runtime environment. The \<^verbatim>\<open>-W\<close> option allows to communicate with
- the Isabelle process via an external program in a more robust fashion.
+ by the ML runtime environment.
\<close>
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Feb 29 16:35:15 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Feb 29 20:43:16 2016 +0100
@@ -159,7 +159,7 @@
my $cmd =
"\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" .
+ "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;' -q $mirabelle_logic" .
$quiet;
my $result = system "bash", "-c", $cmd;
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Mon Feb 29 16:35:15 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Mon Feb 29 20:43:16 2016 +0100
@@ -118,7 +118,7 @@
begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
> $WORKDIR/$LOADER.thy
- "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\"; exit 0;" Pure
+ "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" -q Pure
}
function cleanup_workdir()
--- a/src/Pure/General/file.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/General/file.ML Mon Feb 29 20:43:16 2016 +0100
@@ -45,7 +45,7 @@
(* system path representations *)
val standard_path = Path.implode o Path.expand;
-val platform_path = ml_platform_path o standard_path;
+val platform_path = ML_System.platform_path o standard_path;
val shell_quote = enclose "'" "'";
val shell_path = shell_quote o standard_path;
--- a/src/Pure/ML/exn_properties.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML Mon Feb 29 20:43:16 2016 +0100
@@ -21,7 +21,7 @@
[] => []
| [XML.Text file] =>
if file = "Standard Basis" then []
- else [(Markup.fileN, ml_standard_path file)]
+ else [(Markup.fileN, ML_System.standard_path file)]
| body => XML.Decode.properties body);
fun position_of loc =
--- a/src/Pure/PIDE/batch_session.scala Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala Mon Feb 29 20:43:16 2016 +0100
@@ -58,7 +58,7 @@
case _ =>
}
- prover_session.start("Isabelle", "-r -q " + quote(parent_session))
+ prover_session.start("Isabelle", "-q " + quote(parent_session))
batch_session
}
--- a/src/Pure/PIDE/protocol.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML Mon Feb 29 20:43:16 2016 +0100
@@ -123,8 +123,8 @@
handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
val _ =
- Isabelle_Process.protocol_command "ML_System.share_common_data"
- (fn [] => ML_System.share_common_data ());
+ Isabelle_Process.protocol_command "ML_Heap.share_common_data"
+ (fn [] => ML_Heap.share_common_data ());
end;
--- a/src/Pure/PIDE/session.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/PIDE/session.ML Mon Feb 29 20:43:16 2016 +0100
@@ -13,7 +13,6 @@
(Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
val shutdown: unit -> unit
val finish: unit -> unit
- val save: string -> unit
val protocol_handler: string -> unit
val init_protocol_handlers: unit -> unit
end;
@@ -75,11 +74,6 @@
(Thy_Info.get_names ()) Keyword.empty_keywords;
session_finished := true);
-fun save heap =
- (shutdown ();
- ML_System.share_common_data ();
- ML_System.save_state heap);
-
(** protocol handlers **)
--- a/src/Pure/RAW/ROOT_polyml.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Mon Feb 29 20:43:16 2016 +0100
@@ -29,23 +29,11 @@
end;
-(* ML system operations *)
+(* ML heap operations *)
if ML_System.name = "polyml-5.3.0"
-then use "RAW/share_common_data_polyml-5.3.0.ML"
-else ();
-
-fun ml_platform_path (s: string) = s;
-fun ml_standard_path (s: string) = s;
-
-if ML_System.platform_is_windows then use "RAW/windows_path.ML" else ();
-
-structure ML_System =
-struct
- open ML_System;
- fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
- val save_state = PolyML.SaveState.saveState o ml_platform_path;
-end;
+then use "RAW/ml_heap_polyml-5.3.0.ML"
+else use "RAW/ml_heap.ML";
(* exceptions *)
@@ -183,8 +171,8 @@
PolyML.Compiler.reportUnreferencedIds := true;
PolyML.Compiler.printInAlphabeticalOrder := false;
PolyML.Compiler.maxInlineSize := 80;
-
-fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
+PolyML.Compiler.prompt1 := "ML> ";
+PolyML.Compiler.prompt2 := "ML# ";
use "RAW/ml_parse_tree.ML";
if ML_System.name = "polyml-5.6"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_heap.ML Mon Feb 29 20:43:16 2016 +0100
@@ -0,0 +1,17 @@
+(* Title: Pure/RAW/ml_heap.ML
+ Author: Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+ val share_common_data: unit -> unit
+ val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+ fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+ val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_heap_polyml-5.3.0.ML Mon Feb 29 20:43:16 2016 +0100
@@ -0,0 +1,17 @@
+(* Title: Pure/RAW/ml_heap.ML
+ Author: Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+ val share_common_data: unit -> unit
+ val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+ fun share_common_data () = ();
+ val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
+end;
--- a/src/Pure/RAW/ml_system.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML Mon Feb 29 20:43:16 2016 +0100
@@ -9,20 +9,50 @@
val name: string
val platform: string
val platform_is_windows: bool
- val share_common_data: unit -> unit
- val save_state: string -> unit
+ val platform_path: string -> string
+ val standard_path: string -> string
end;
structure ML_System: ML_SYSTEM =
struct
val SOME name = OS.Process.getEnv "ML_SYSTEM";
-
val SOME platform = OS.Process.getEnv "ML_PLATFORM";
val platform_is_windows = String.isSuffix "windows" platform;
-fun share_common_data () = ();
-fun save_state _ = raise Fail "Cannot save state -- undefined operation";
+val platform_path =
+ if platform_is_windows then
+ fn path =>
+ if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
+ (case String.tokens (fn c => c = #"/") path of
+ "cygdrive" :: drive :: arcs =>
+ let
+ val vol =
+ (case Char.fromString drive of
+ NONE => drive ^ ":"
+ | SOME d => String.str (Char.toUpper d) ^ ":");
+ in String.concatWith "\\" (vol :: arcs) end
+ | arcs =>
+ (case OS.Process.getEnv "CYGWIN_ROOT" of
+ SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
+ | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
+ else String.translate (fn #"/" => "\\" | c => String.str c) path
+ else fn path => path;
+
+val standard_path =
+ if platform_is_windows then
+ fn path =>
+ let
+ val {vol, arcs, isAbs} = OS.Path.fromString path;
+ val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
+ in
+ if isAbs then
+ (case String.explode vol of
+ [d, #":"] =>
+ String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
+ | _ => path')
+ else path'
+ end
+ else fn path => path;
end;
-
--- a/src/Pure/RAW/share_common_data_polyml-5.3.0.ML Mon Feb 29 16:35:15 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: Pure/RAW/share_common_data_polyml-5.3.0.ML
-
-Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
-anymore.
-*)
-
-structure PolyML =
-struct
- open PolyML;
- fun shareCommonData _ = ();
-end;
--- a/src/Pure/RAW/windows_path.ML Mon Feb 29 16:35:15 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Title: Pure/RAW/windows_path.ML
- Author: Makarius
-
-Windows file-system paths.
-*)
-
-fun ml_platform_path path =
- if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
- (case String.tokens (fn c => c = #"/") path of
- "cygdrive" :: drive :: arcs =>
- let
- val vol =
- (case Char.fromString drive of
- NONE => drive ^ ":"
- | SOME d => String.str (Char.toUpper d) ^ ":");
- in String.concatWith "\\" (vol :: arcs) end
- | arcs =>
- (case OS.Process.getEnv "CYGWIN_ROOT" of
- SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
- | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
- else String.translate (fn #"/" => "\\" | c => String.str c) path;
-
-fun ml_standard_path path =
- let
- val {vol, arcs, isAbs} = OS.Path.fromString path;
- val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
- in
- if isAbs then
- (case String.explode vol of
- [d, #":"] =>
- String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
- | _ => path')
- else path'
- end;
--- a/src/Pure/ROOT Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/ROOT Mon Feb 29 20:43:16 2016 +0100
@@ -14,6 +14,8 @@
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
"RAW/ml_debugger_polyml-5.6.ML"
+ "RAW/ml_heap.ML"
+ "RAW/ml_heap_polyml-5.3.0.ML"
"RAW/ml_name_space_polyml-5.6.ML"
"RAW/ml_name_space_polyml.ML"
"RAW/ml_parse_tree.ML"
@@ -26,11 +28,9 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
- "RAW/share_common_data_polyml-5.3.0.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
"RAW/use_context.ML"
- "RAW/windows_path.ML"
session Pure =
global_theories Pure
@@ -46,6 +46,8 @@
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
"RAW/ml_debugger_polyml-5.6.ML"
+ "RAW/ml_heap.ML"
+ "RAW/ml_heap_polyml-5.3.0.ML"
"RAW/ml_name_space_polyml-5.6.ML"
"RAW/ml_name_space_polyml.ML"
"RAW/ml_parse_tree.ML"
@@ -58,11 +60,9 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
- "RAW/share_common_data_polyml-5.3.0.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
"RAW/use_context.ML"
- "RAW/windows_path.ML"
"Concurrent/bash.ML"
"Concurrent/bash_windows.ML"
--- a/src/Pure/System/command_line.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/System/command_line.ML Mon Feb 29 20:43:16 2016 +0100
@@ -19,7 +19,7 @@
val rc =
restore_attributes body () handle exn =>
Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
- in if rc = 0 then () else exit rc end) ();
+ in exit rc end) ();
fun tool0 body = tool (fn () => (body (); 0));
--- a/src/Pure/Tools/build.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/Tools/build.ML Mon Feb 29 20:43:16 2016 +0100
@@ -124,15 +124,16 @@
let
val _ = SHA1_Samples.test ();
- val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info,
+ val (symbol_codes, (command_timings, (output, (options, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
- pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode
+ pair (list (pair string int)) (pair (list properties) (pair string (pair Options.decode
(pair bool (pair string (pair (list (pair string string)) (pair string
(pair string (pair string (pair string
((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
end;
+ val do_output = output <> "";
val symbols = HTML.make_symbols symbol_codes;
val _ = Options.set_default options;
@@ -165,7 +166,7 @@
val _ = Par_Exn.release_all [res1, res2];
val _ = Options.reset_default ();
- val _ = if do_output then () else exit 0;
+ val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else ();
in () end);
--- a/src/Pure/Tools/build.scala Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/Tools/build.scala Mon Feb 29 20:43:16 2016 +0100
@@ -541,6 +541,7 @@
browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
{
def output_path: Option[Path] = if (do_output) Some(output) else None
+ def output_standard_path: String = if (do_output) File.standard_path(output) else ""
private val parent = info.parent.getOrElse("")
@@ -555,25 +556,25 @@
{
val theories = info.theories.map(x => (x._2, x._3))
import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Options.encode,
+ pair(list(pair(string, int)), pair(list(properties), pair(string, pair(Options.encode,
pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string,
list(pair(Options.encode, list(Path.encode))))))))))))))(
- (Symbol.codes, (command_timings, (do_output, (info.options,
+ (Symbol.codes, (command_timings, (output_standard_path, (info.options,
(verbose, (browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name,
theories))))))))))))
}))
private val env =
- Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output),
+ Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
(if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
File.standard_path(args_file))
private val script =
if (is_pure(name)) {
if (do_output) "./build " + name + " \"$OUTPUT\""
- else """ rm -f "$OUTPUT"; ./build """ + name
+ else "./build " + name
}
else {
"""
@@ -581,11 +582,13 @@
""" +
(if (do_output)
"""
- "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
+ rm -f "$OUTPUT"
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT"
"""
else
"""
- rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
+ rm -f "$OUTPUT"
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT"
""") +
"""
RC="$?"
--- a/src/Pure/build Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/build Mon Feb 29 20:43:16 2016 +0100
@@ -64,11 +64,11 @@
-e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
-q RAW_ML_SYSTEM
else
+ rm -f "$OUTPUT"
"$ISABELLE_PROCESS" \
-e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
- -e "structure Isar = struct fun main () = () end;" \
- -e "ml_prompts \"ML> \" \"ML# \";" \
- -q -w RAW_ML_SYSTEM "$OUTPUT"
+ -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
+ -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
fi
else
if [ -z "$OUTPUT" ]; then
@@ -76,12 +76,11 @@
-e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
-q RAW_ML_SYSTEM
else
+ rm -f "$OUTPUT"
"$ISABELLE_PROCESS" \
-e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
- -e "ml_prompts \"ML> \" \"ML# \";" \
- -e "Command_Line.tool0 Session.finish;" \
- -e "Options.reset_default ();" \
- -q -w RAW_ML_SYSTEM "$OUTPUT"
+ -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
+ -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
fi
fi
--- a/src/Pure/library.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Pure/library.ML Mon Feb 29 20:43:16 2016 +0100
@@ -1031,8 +1031,8 @@
(* current directory *)
-val cd = OS.FileSys.chDir o ml_platform_path;
-val pwd = ml_standard_path o OS.FileSys.getDir;
+val cd = OS.FileSys.chDir o ML_System.platform_path;
+val pwd = ML_System.standard_path o OS.FileSys.getDir;
(* getenv *)
--- a/src/Tools/Code/code_ml.ML Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Tools/Code/code_ml.ML Mon Feb 29 20:43:16 2016 +0100
@@ -869,7 +869,7 @@
check = { env_var = "ISABELLE_PROCESS",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
+ "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
#> Code_Target.add_language
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "ISABELLE_OCAML",
--- a/src/Tools/jEdit/src/isabelle_logic.scala Mon Feb 29 16:35:15 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Mon Feb 29 20:43:16 2016 +0100
@@ -74,7 +74,7 @@
val print_modes =
(space_explode(',', PIDE.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _)
- (print_modes ::: List("-r", "-q", File.shell_quote(session_name()))).mkString(" ")
+ (print_modes ::: List("-q", File.shell_quote(session_name()))).mkString(" ")
}
def session_start(): Unit = PIDE.session.start("Isabelle", session_args())