1.1 --- a/src/Pure/System/build.ML	Mon Jul 23 22:35:10 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 00:29:36 2012 +0200
     1.3 @@ -12,14 +12,43 @@
     1.4  structure Build: BUILD =
     1.5  struct
     1.6  
     1.7 +fun use_theories name options =
     1.8 +  Thy_Info.use_thys
     1.9 +    |> Session.with_timing name (Options.bool options "timing")
    1.10 +    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    1.11 +    |> Unsynchronized.setmp print_mode
    1.12 +        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    1.13 +    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    1.14 +    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    1.15 +        (Options.int options "parallel_proofs_threshold")
    1.16 +    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.17 +    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit");
    1.18 +
    1.19  fun build args_file =
    1.20    let
    1.21 -    val (save, (parent, (name, theories))) =
    1.22 +    val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) =
    1.23        File.read (Path.explode args_file) |> YXML.parse_body |>
    1.24 -        let open XML.Decode in pair bool (pair string (pair string (list string))) end;
    1.25 +        let open XML.Decode in
    1.26 +          pair bool (pair Options.decode (pair bool (pair string (pair string
    1.27 +            (pair string (pair string ((list (pair Options.decode (list string))))))))))
    1.28 +        end;
    1.29  
    1.30 -    val _ = Session.init false parent name;  (* FIXME reset!? *)
    1.31 -    val _ = Thy_Info.use_thys theories;
    1.32 +    val _ =
    1.33 +      Session.init
    1.34 +        save
    1.35 +        false (* FIXME reset!? *)
    1.36 +        (Options.bool options "browser_info") browser_info
    1.37 +        (Options.string options "document_format")   (* FIXME dependent on "document" (!?) *)
    1.38 +        (Options.bool options "document_graph")
    1.39 +        (space_explode "," (Options.string options "document_variants"))
    1.40 +        parent
    1.41 +        base_name
    1.42 +        (true (* FIXME copy document/ files on Scala side!? *),
    1.43 +          Options.string options "document_dump")
    1.44 +        ""
    1.45 +        verbose;
    1.46 +
    1.47 +    val _ = List.app (uncurry (use_theories name)) theories;
    1.48      val _ = Session.finish ();
    1.49  
    1.50      val _ = if save then () else quit ();