# HG changeset patch
# User wenzelm
# Date 1343082576 -7200
# Node ID fd9e28d5a14352b79f732a6701242e14d1e8acbb
# Parent  d8ff14f44a40a1264c04ac40236548dfb1e85a6b
pass build options to ML;
some imitation of usedir Session.init;

diff -r d8ff14f44a40 -r fd9e28d5a143 etc/options
--- a/etc/options	Mon Jul 23 22:35:10 2012 +0200
+++ b/etc/options	Tue Jul 24 00:29:36 2012 +0200
@@ -6,6 +6,7 @@
 declare document_format : string = pdf
 declare document_variants : string = document
 declare document_graph : bool = false
+declare document_dump : string = ""
 
 declare threads_limit : int = 1
 declare threads_trace : int = 0
@@ -18,7 +19,6 @@
 declare quick_and_dirty : bool = false
 
 declare timing : bool = false
-declare verbose : bool = false
 
 declare condition : string = ""
 
diff -r d8ff14f44a40 -r fd9e28d5a143 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/General/path.scala	Tue Jul 24 00:29:36 2012 +0200
@@ -98,6 +98,11 @@
 
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
+
+
+  /* encode */
+
+  val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
 }
 
 
diff -r d8ff14f44a40 -r fd9e28d5a143 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 00:29:36 2012 +0200
@@ -12,14 +12,43 @@
 structure Build: BUILD =
 struct
 
+fun use_theories name options =
+  Thy_Info.use_thys
+    |> Session.with_timing name (Options.bool options "timing")
+    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
+    |> Unsynchronized.setmp print_mode
+        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
+        (Options.int options "parallel_proofs_threshold")
+    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit");
+
 fun build args_file =
   let
-    val (save, (parent, (name, theories))) =
+    val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) =
       File.read (Path.explode args_file) |> YXML.parse_body |>
-        let open XML.Decode in pair bool (pair string (pair string (list string))) end;
+        let open XML.Decode in
+          pair bool (pair Options.decode (pair bool (pair string (pair string
+            (pair string (pair string ((list (pair Options.decode (list string))))))))))
+        end;
 
-    val _ = Session.init false parent name;  (* FIXME reset!? *)
-    val _ = Thy_Info.use_thys theories;
+    val _ =
+      Session.init
+        save
+        false (* FIXME reset!? *)
+        (Options.bool options "browser_info") browser_info
+        (Options.string options "document_format")   (* FIXME dependent on "document" (!?) *)
+        (Options.bool options "document_graph")
+        (space_explode "," (Options.string options "document_variants"))
+        parent
+        base_name
+        (true (* FIXME copy document/ files on Scala side!? *),
+          Options.string options "document_dump")
+        ""
+        verbose;
+
+    val _ = List.app (uncurry (use_theories name)) theories;
     val _ = Session.finish ();
 
     val _ = if save then () else quit ();
diff -r d8ff14f44a40 -r fd9e28d5a143 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 24 00:29:36 2012 +0200
@@ -42,6 +42,7 @@
     /* Info */
 
     sealed case class Info(
+      base_name: String,
       dir: Path,
       parent: Option[String],
       description: String,
@@ -214,7 +215,7 @@
         val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
 
         val info =
-          Session.Info(dir + path, entry.parent,
+          Session.Info(entry.name, dir + path, entry.parent,
             entry.description, options ++ entry.options, theories, files, digest)
 
         queue1 + (key, info)
@@ -340,7 +341,8 @@
     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   }
 
-  private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
+  private def start_job(name: String, info: Session.Info, output: Option[String],
+    options: Options, verbose: Boolean, browser_info: Path): Job =
   {
     val parent = info.parent.getOrElse("")
 
@@ -371,8 +373,10 @@
     val args_xml =
     {
       import XML.Encode._
-      pair(bool, pair(string, pair(string, list(string))))(
-        output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
+          pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
+            pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+          (output.isDefined, (options, (verbose, (browser_info, (parent,
+            (name, (info.base_name, info.theories))))))))
     }
     new Job(cwd, env, script, YXML.string_of_body(args_xml))
   }
@@ -454,7 +458,7 @@
                   Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
                 else None
               echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
-              val job = start_job(name, info, output)
+              val job = start_job(name, info, output, options, verbose, browser_info)
               loop(pending, running + (name -> job), results)
             }
             else {
diff -r d8ff14f44a40 -r fd9e28d5a143 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Jul 24 00:29:36 2012 +0200
@@ -79,6 +79,11 @@
     }
     options
   }
+
+
+  /* encode */
+
+  val encode: XML.Encode.T[Options] = (options => options.encode)
 }
 
 
diff -r d8ff14f44a40 -r fd9e28d5a143 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/session.ML	Tue Jul 24 00:29:36 2012 +0200
@@ -9,11 +9,13 @@
   val id: unit -> string list
   val name: unit -> string
   val welcome: unit -> string
-  val init: bool -> string -> string -> unit
+  val finish: unit -> unit
+  val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
+    string -> string -> bool * string -> string -> bool -> unit
+  val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
-  val finish: unit -> unit
 end;
 
 structure Session: SESSION =
@@ -63,9 +65,9 @@
   end;
 
 
-(* init *)
+(* init_name *)
 
-fun init reset parent name =
+fun init_name reset parent name =
   if not (member (op =) (! session) parent) orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
   else (add_path reset name; session_finished := false);
@@ -94,26 +96,31 @@
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
+fun with_timing _ false f x = f x
+  | with_timing item true f x =
+      let
+        val start = Timing.start ();
+        val y = f x;
+        val timing = Timing.result start;
+        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
+          |> Real.fmt (StringCvt.FIX (SOME 2));
+        val _ =
+          Output.physical_stderr ("Timing " ^ item ^ " (" ^
+            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
+            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
+      in y end;
+
+fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
+ (init_name reset parent name;
+  Present.init build info info_path doc doc_graph doc_variants (path ()) name
+    (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())));
+
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
-     (init reset parent name;
-      Present.init build info info_path doc doc_graph doc_variants (path ()) name
-        (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
-      if timing then
-        let
-          val start = Timing.start ();
-          val _ = use root;
-          val timing = Timing.result start;
-          val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
-            |> Real.fmt (StringCvt.FIX (SOME 2));
-          val _ =
-            Output.physical_stderr ("Timing " ^ item ^ " (" ^
-              string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
-              Timing.message timing ^ ", factor " ^ factor ^ ")\n");
-        in () end
-      else use root;
+     (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose;
+      with_timing item timing use root;
       finish ()))
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())