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;