# HG changeset patch
# User wenzelm
# Date 1368363915 -7200
# Node ID ead4248aef3bcc5c3be75cba8f9d47d7934cc7f6
# Parent  958d439b3013fc6244bffe8e5eadb99f9ea0d398
full default options for Isabelle_Process and Build;

diff -r 958d439b3013 -r ead4248aef3b src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sun May 12 14:25:16 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun May 12 15:05:15 2013 +0200
@@ -237,6 +237,7 @@
   protocol_command "Isabelle_Process.options"
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
+        Options.set_default options;
         Future.ML_statistics := true;
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads := Options.int options "threads";
diff -r 958d439b3013 -r ead4248aef3b src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun May 12 14:25:16 2013 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 12 15:05:15 2013 +0200
@@ -109,7 +109,9 @@
 fun use_theories_condition last_timing (options, thys) =
   let val condition = space_explode "," (Options.string options "condition") in
     (case filter_out (can getenv_strict) condition of
-      [] => use_theories last_timing options (map (rpair Position.none) thys)
+      [] =>
+        (Options.set_default options;
+         use_theories last_timing options (map (rpair Position.none) thys))
     | conds =>
         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
           " (undefined " ^ commas conds ^ ")\n"))
@@ -128,6 +130,8 @@
                 ((list (pair Options.decode (list string)))))))))))
           end;
 
+      val _ = Options.set_default options;
+
       val document_variants =
         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
       val _ =
@@ -160,6 +164,7 @@
       val res2 = Exn.capture Session.finish ();
       val _ = Par_Exn.release_all [res1, res2];
 
+      val _ = Options.reset_default ();
       val _ = if do_output then () else exit 0;
     in 0 end);