src/Pure/System/build.ML
author wenzelm
Tue Jul 24 11:02:42 2012 +0200 (2012-07-24)
changeset 48463 07f752935ece
parent 48462 424fd5364f15
child 48464 a7bf1587eba0
permissions -rw-r--r--
added "browser_info_remote" (cf. usedir -P);
     1 (*  Title:      Pure/System/build.ML
     2     Author:     Makarius
     3 
     4 Build Isabelle sessions.
     5 *)
     6 
     7 signature BUILD =
     8 sig
     9   val build: string -> unit
    10 end;
    11 
    12 structure Build: BUILD =
    13 struct
    14 
    15 fun use_theories options =
    16   Thy_Info.use_thys
    17     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    18     |> Unsynchronized.setmp print_mode
    19         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    20     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    21     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    22         (Options.int options "parallel_proofs_threshold")
    23     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    24     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    25     |> Options.bool options "no_document" ? Present.no_document;
    26 
    27 fun build args_file =
    28   let
    29     val (save, (options, (timing, (verbose, (browser_info, (parent,
    30         (name, (base_name, theories)))))))) =
    31       File.read (Path.explode args_file) |> YXML.parse_body |>
    32         let open XML.Decode in
    33           pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
    34             (pair string (pair string ((list (pair Options.decode (list string)))))))))))
    35         end;
    36 
    37     val _ =
    38       Session.init save false
    39         (Options.bool options "browser_info") browser_info
    40         (Options.string options "document")
    41         (Options.bool options "document_graph")
    42         (space_explode "," (Options.string options "document_variants"))
    43         parent base_name
    44         (true (* FIXME copy document/ files on Scala side!? *),
    45           Options.string options "document_dump")
    46         (Options.string options "browser_info_remote")
    47         verbose;
    48 
    49     val _ = Session.with_timing name timing (List.app (uncurry use_theories)) theories;
    50     val _ = Session.finish ();
    51 
    52     val _ = if save then () else quit ();
    53   in () end
    54   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    55 
    56 end;