src/Pure/System/build.ML
author wenzelm
Thu Jul 26 19:41:05 2012 +0200 (2012-07-26)
changeset 48527 4ee8d70cd5a3
parent 48520 6d4ea2efa64b
child 48541 f31ef1a0285a
permissions -rw-r--r--
more build options;
     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 Thy_Output.display_default (Options.bool options "thy_output_display")
    39     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    40     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    41     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    42     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    43     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    44     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    45 
    46 fun use_theories (options, thys) =
    47   let val condition = space_explode "," (Options.string options "condition") in
    48     (case filter_out (can getenv_strict) condition of
    49       [] => use_thys options thys
    50     | conds =>
    51         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    52           " (undefined " ^ commas conds ^ ")\n"))
    53   end;
    54 
    55 in
    56 
    57 fun build args_file =
    58   let
    59     val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
    60         (name, (base_name, theories)))))))) =
    61       File.read (Path.explode args_file) |> YXML.parse_body |>
    62         let open XML.Decode in
    63           pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
    64             (pair string (pair string ((list (pair Options.decode (list string)))))))))))
    65         end;
    66 
    67     val _ =
    68       Session.init do_output false
    69         (Options.bool options "browser_info") browser_info
    70         (Options.string options "document")
    71         (Options.bool options "document_graph")
    72         (space_explode ":" (Options.string options "document_variants"))
    73         parent_base_name base_name
    74         (Options.string options "document_dump", Options.string options "document_dump_mode")
    75         "" verbose;
    76     val _ = Session.with_timing name timing (List.app use_theories) theories;
    77     val _ = Session.finish ();
    78     val _ = if do_output then () else quit ();
    79   in () end
    80   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    81 
    82 end;
    83 
    84 end;