load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
--- a/bin/isabelle-process Sun May 12 18:22:44 2013 +0200
+++ b/bin/isabelle-process Sun May 12 19:56:30 2013 +0200
@@ -58,7 +58,7 @@
# options
-ISAR=false
+ISAR=""
PROOFGENERAL=""
SECURE=""
WRAPPER_SOCKET=""
@@ -76,7 +76,6 @@
ISAR=true
;;
P)
- ISAR=true
PROOFGENERAL=true
;;
S)
@@ -210,7 +209,7 @@
[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
-[ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
+[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
NICE="nice"
@@ -222,18 +221,21 @@
[ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
[ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
-elif [ "$ISAR" = true ]; then
+else
if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
"$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
fi
+ if [ "$INPUT" != RAW_ML_SYSTEM ]; then
+ MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
+ fi
if [ -n "$PROOFGENERAL" ]; then
MLTEXT="$MLTEXT; ProofGeneral.init ();"
+ elif [ -n "$ISAR" ]; then
+ MLTEXT="$MLTEXT; Isar.main ();"
else
- MLTEXT="$MLTEXT; Isar.main ();"
+ NICE=""
fi
-else
- NICE=""
fi
export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
--- a/src/Pure/System/isar.ML Sun May 12 18:22:44 2013 +0200
+++ b/src/Pure/System/isar.ML Sun May 12 19:56:30 2013 +0200
@@ -155,7 +155,7 @@
fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
(Context.set_thread_data NONE;
- if do_init then (Options.load_default (); init ()) else ();
+ if do_init then init () else ();
Output.Private_Hooks.protocol_message_fn := protocol_message;
if welcome then writeln (Session.welcome ()) else ();
uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
--- a/src/Pure/System/session.ML Sun May 12 18:22:44 2013 +0200
+++ b/src/Pure/System/session.ML Sun May 12 19:56:30 2013 +0200
@@ -112,7 +112,9 @@
parent ("Unsorted", name) doc_dump verbose;
val res1 = (use |> with_timing item timing |> Exn.capture) root;
val res2 = Exn.capture finish ();
- in ignore (Par_Exn.release_all [res1, res2]) end)
+ val _ = ignore (Par_Exn.release_all [res1, res2]);
+ val _ = Options.reset_default ();
+ in () end)
|> Unsynchronized.setmp Proofterm.proofs level
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
|> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs