src/Pure/System/build.ML
author wenzelm
Thu Jul 26 14:29:54 2012 +0200 (2012-07-26)
changeset 48516 c5d0f19ef7cb
parent 48513 ace120a2cb70
child 48520 6d4ea2efa64b
permissions -rw-r--r--
refined "document_dump_mode": "all", "tex+sty", "tex";
     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 local
    16 
    17 fun no_document options =
    18   (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso
    19   (Options.string options "document_dump" = "");
    20 
    21 fun use_thys options =
    22   Thy_Info.use_thys
    23     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    24     |> Unsynchronized.setmp print_mode
    25         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    26     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    27     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    28         (Options.int options "parallel_proofs_threshold")
    29     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    30     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    31     |> no_document options ? Present.no_document
    32     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    33     |> Unsynchronized.setmp Printer.show_question_marks_default
    34         (Options.bool options "show_question_marks")
    35     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    36     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    37     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    38     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    39 
    40 fun use_theories (options, thys) =
    41   let val condition = space_explode "," (Options.string options "condition") in
    42     (case filter_out (can getenv_strict) condition of
    43       [] => use_thys options thys
    44     | conds =>
    45         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    46           " (undefined " ^ commas conds ^ ")\n"))
    47   end;
    48 
    49 in
    50 
    51 fun build args_file =
    52   let
    53     val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
    54         (name, (base_name, theories)))))))) =
    55       File.read (Path.explode args_file) |> YXML.parse_body |>
    56         let open XML.Decode in
    57           pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
    58             (pair string (pair string ((list (pair Options.decode (list string)))))))))))
    59         end;
    60 
    61     val _ =
    62       Session.init do_output false
    63         (Options.bool options "browser_info") browser_info
    64         (Options.string options "document")
    65         (Options.bool options "document_graph")
    66         (space_explode ":" (Options.string options "document_variants"))
    67         parent_base_name base_name
    68         (Options.string options "document_dump", Options.string options "document_dump_mode")
    69         "" verbose;
    70     val _ = Session.with_timing name timing (List.app use_theories) theories;
    71     val _ = Session.finish ();
    72     val _ = if do_output then () else quit ();
    73   in () end
    74   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    75 
    76 end;
    77 
    78 end;