# HG changeset patch
# User wenzelm
# Date 1368381390 -7200
# Node ID cb5dbc9a06f95cb06c87e20606d0ae6b3b570f8d
# Parent  3301612c48939136e1a0b8343e841da634e5f7e1
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;

diff -r 3301612c4893 -r cb5dbc9a06f9 bin/isabelle-process
--- 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
diff -r 3301612c4893 -r cb5dbc9a06f9 src/Pure/System/isar.ML
--- 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)) ());
diff -r 3301612c4893 -r cb5dbc9a06f9 src/Pure/System/session.ML
--- 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