# HG changeset patch
# User wenzelm
# Date 1344280302 -7200
# Node ID 2585042b1a307c25b6dc1eae2d245167ebaa8938
# Parent  538ea0adb8e109b7d8c27dfe2a5cafc473c61af8
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;

diff -r 538ea0adb8e1 -r 2585042b1a30 bin/isabelle-process
--- a/bin/isabelle-process	Mon Aug 06 17:54:05 2012 +0200
+++ b/bin/isabelle-process	Mon Aug 06 21:11:42 2012 +0200
@@ -231,12 +231,16 @@
 elif [ -n "$PROOFGENERAL" ]; then
   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
 elif [ "$ISAR" = true ]; then
-  MLTEXT="$MLTEXT; Isar.main();"
+  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
+  MLTEXT="$MLTEXT; Isar.main ();"
 else
   NICE=""
 fi
 
-export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
+export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
@@ -245,6 +249,7 @@
 fi
 RC="$?"
 
+[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
 rmdir "$ISABELLE_TMP"
 
 exit "$RC"
diff -r 538ea0adb8e1 -r 2585042b1a30 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Mon Aug 06 17:54:05 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Aug 06 21:11:42 2012 +0200
@@ -406,8 +406,23 @@
 
     private val parent = info.parent.getOrElse("")
 
+    private val args_file = File.tmp_file("args")
+    File.write(args_file, YXML.string_of_body(
+      if (is_pure(name)) Options.encode(info.options)
+      else
+        {
+          import XML.Encode._
+              pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
+                pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
+              (do_output, (info.options, (verbose, (browser_info, (parent,
+                (name, info.theories)))))))
+        }))
+
     private val env =
-      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
+      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
+        (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
+          Isabelle_System.posix_path(args_file.getPath))
+
     private val script =
       if (is_pure(name)) {
         if (do_output) "./build " + name + " \"$OUTPUT\""
@@ -437,20 +452,9 @@
         exit "$RC"
         """
       }
-    private val args_xml =
-    {
-      import XML.Encode._
-          pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
-            pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
-          (do_output, (info.options, (verbose, (browser_info, (parent,
-            (name, info.theories)))))))
-    }
-    private val args_file = File.tmp_file("args")
-    private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
-    File.write(args_file, YXML.string_of_body(args_xml))
 
     private val (thread, result) =
-      Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env1, script) }
+      Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
 
     def terminate: Unit = thread.interrupt
     def is_finished: Boolean = result.is_finished
diff -r 538ea0adb8e1 -r 2585042b1a30 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Mon Aug 06 17:54:05 2012 +0200
+++ b/src/Pure/System/isar.ML	Mon Aug 06 21:11:42 2012 +0200
@@ -137,7 +137,7 @@
 
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  if do_init then init () else ();
+  if do_init then (Options.load_default (); init ()) else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
diff -r 538ea0adb8e1 -r 2585042b1a30 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Mon Aug 06 17:54:05 2012 +0200
+++ b/src/Pure/System/options.ML	Mon Aug 06 21:11:42 2012 +0200
@@ -14,6 +14,10 @@
   val string: T -> string -> string
   val declare: {name: string, typ: string, value: string} -> T -> T
   val decode: XML.body -> T
+  val default: unit -> T
+  val set_default: T -> unit
+  val reset_default: unit -> unit
+  val load_default: unit -> unit
 end;
 
 structure Options: OPTIONS =
@@ -72,5 +76,31 @@
   fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
     (let open XML.Decode in list (triple string string string) end body) empty;
 
+
+
+(** global default **)
+
+val global_default = Synchronized.var "Options.default" (NONE: T option);
+
+fun default () =
+  (case Synchronized.value global_default of
+    SOME options => options
+  | NONE => error "No global default options");
+
+fun set_default options = Synchronized.change global_default (K (SOME options));
+fun reset_default () = Synchronized.change global_default (K NONE);
+
+fun load_default () =
+  (case getenv "ISABELLE_PROCESS_OPTIONS" of
+    "" => ()
+  | name =>
+      let val path = Path.explode name in
+        (case try File.read path of
+          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
+        | NONE => ())
+      end);
+
+val _ = load_default ();
+
 end;
 
diff -r 538ea0adb8e1 -r 2585042b1a30 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Aug 06 17:54:05 2012 +0200
+++ b/src/Pure/System/session.ML	Mon Aug 06 21:11:42 2012 +0200
@@ -73,6 +73,7 @@
     Present.finish ();
     Outer_Syntax.check_syntax ();
     Future.shutdown ();
+    Options.reset_default ();
     session_finished := true);