--- a/NEWS Mon Feb 29 16:38:06 2016 +0100
+++ b/NEWS Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/bin/isabelle_process Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/lib/scripts/run-polyml Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/lib/scripts/run-polyml-5.3.0 Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/src/Doc/System/Basics.thy Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Mon Feb 29 20:35:06 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/PIDE/batch_session.scala Mon Feb 29 16:38:06 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala Mon Feb 29 20:35:06 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/Tools/build.scala Mon Feb 29 16:38:06 2016 +0100
+++ b/src/Pure/Tools/build.scala Mon Feb 29 20:35:06 2016 +0100
@@ -583,12 +583,12 @@
(if (do_output)
"""
rm -f "$OUTPUT"
- "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" && chmod -w "$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"
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT"
""") +
"""
RC="$?"
--- a/src/Tools/Code/code_ml.ML Mon Feb 29 16:38:06 2016 +0100
+++ b/src/Tools/Code/code_ml.ML Mon Feb 29 20:35:06 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:38:06 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Mon Feb 29 20:35:06 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())