# HG changeset patch # User wenzelm # Date 1456774996 -3600 # Node ID d396da07055db77bd5c19c207fff0ec188b619d6 # Parent 87ca8b5145b870c33d3179909bee11ccfbb0109d# Parent 43e64c770f28695b3671aff7e1ba6d3702dd1fa4 merged diff -r 87ca8b5145b8 -r d396da07055d NEWS --- 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. diff -r 87ca8b5145b8 -r d396da07055d bin/isabelle_process --- 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" diff -r 87ca8b5145b8 -r d396da07055d lib/scripts/run-polyml --- 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 (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: diff -r 87ca8b5145b8 -r d396da07055d src/Doc/System/Basics.thy --- 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 \ 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] -\Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT] +\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.\} + 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.\} - 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 \Options\ text \ - If the input heap file does not have write permission bits set, or the \<^verbatim>\-r\ - 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>\-w\ 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>\-e\ option, arbitrary ML code may be passed to the Isabelle session from the command line. Multiple \<^verbatim>\-e\ 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] \isabelle_process\} - Usually @{setting ISABELLE_LOGIC} refers to one of the standard logic - images, which are read-only by default. A writable session --- based on - \<^verbatim>\HOL\, but output to \<^verbatim>\Test\ (in the directory specified by the @{setting - ISABELLE_OUTPUT} setting) --- may be invoked as follows: - @{verbatim [display] \isabelle_process HOL Test\} - - Ending this session normally (e.g.\ by typing control-D) dumps the whole ML - system state into \<^verbatim>\Test\ (be prepared for more than 100\,MB): - - The \<^verbatim>\Test\ session may be continued later (still in writable state) by: - @{verbatim [display] \isabelle_process Test\} - - A read-only \<^verbatim>\Test\ session may be started by: - @{verbatim [display] \isabelle_process -r Test\} - - \<^bigskip> + \<^medskip> The next example demonstrates batch execution of Isabelle. We retrieve the \<^verbatim>\Main\ theory value from the theory loader within ML (observe the delicate quoting rules for the Bash shell vs.\ ML): - @{verbatim [display] \isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL\} + @{verbatim [display] \isabelle_process -e 'Thy_Info.get_theory "Main";' -q HOL\} Note that the output text will be interspersed with additional junk messages - by the ML runtime environment. The \<^verbatim>\-W\ option allows to communicate with - the Isabelle process via an external program in a more robust fashion. + by the ML runtime environment. \ diff -r 87ca8b5145b8 -r d396da07055d src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- 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; diff -r 87ca8b5145b8 -r d396da07055d src/HOL/TPTP/lib/Tools/tptp_graph --- 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() diff -r 87ca8b5145b8 -r d396da07055d src/Pure/General/file.ML --- 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; diff -r 87ca8b5145b8 -r d396da07055d src/Pure/ML/exn_properties.ML --- 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 = diff -r 87ca8b5145b8 -r d396da07055d src/Pure/PIDE/batch_session.scala --- 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 } diff -r 87ca8b5145b8 -r d396da07055d src/Pure/PIDE/protocol.ML --- 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; diff -r 87ca8b5145b8 -r d396da07055d src/Pure/PIDE/session.ML --- 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 **) diff -r 87ca8b5145b8 -r d396da07055d src/Pure/RAW/ROOT_polyml.ML --- 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" diff -r 87ca8b5145b8 -r d396da07055d src/Pure/RAW/ml_heap.ML --- /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; diff -r 87ca8b5145b8 -r d396da07055d src/Pure/RAW/ml_heap_polyml-5.3.0.ML --- /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; diff -r 87ca8b5145b8 -r d396da07055d src/Pure/RAW/ml_system.ML --- 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; - diff -r 87ca8b5145b8 -r d396da07055d src/Pure/RAW/share_common_data_polyml-5.3.0.ML --- 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; diff -r 87ca8b5145b8 -r d396da07055d src/Pure/RAW/windows_path.ML --- 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; diff -r 87ca8b5145b8 -r d396da07055d src/Pure/ROOT --- 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" diff -r 87ca8b5145b8 -r d396da07055d src/Pure/System/command_line.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)); diff -r 87ca8b5145b8 -r d396da07055d src/Pure/Tools/build.ML --- 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); diff -r 87ca8b5145b8 -r d396da07055d src/Pure/Tools/build.scala --- 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="$?" diff -r 87ca8b5145b8 -r d396da07055d src/Pure/build --- 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 diff -r 87ca8b5145b8 -r d396da07055d src/Pure/library.ML --- 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 *) diff -r 87ca8b5145b8 -r d396da07055d src/Tools/Code/code_ml.ML --- 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", diff -r 87ca8b5145b8 -r d396da07055d src/Tools/jEdit/src/isabelle_logic.scala --- 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())