src/Pure/System/build.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48634 30a6e841390a
child 48662 b171bcd5dd86
permissions -rw-r--r--
more official command specifications, including source position;
     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 Toplevel.skip_proofs (Options.bool options "skip_proofs")
    34     |> Unsynchronized.setmp Printer.show_question_marks_default
    35         (Options.bool options "show_question_marks")
    36     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    37     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    38     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    39     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    40     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    41     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    42     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    43     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    44     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    45     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    46 
    47 fun use_theories (options, thys) =
    48   let val condition = space_explode "," (Options.string options "condition") in
    49     (case filter_out (can getenv_strict) condition of
    50       [] => use_thys options thys
    51     | conds =>
    52         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    53           " (undefined " ^ commas conds ^ ")\n"))
    54   end;
    55 
    56 in
    57 
    58 fun build args_file =
    59   let
    60     val (do_output, (options, (verbose, (browser_info, (parent_name,
    61         (name, theories)))))) =
    62       File.read (Path.explode args_file) |> YXML.parse_body |>
    63         let open XML.Decode in
    64           pair bool (pair Options.decode (pair bool (pair string (pair string
    65             (pair string ((list (pair Options.decode (list string)))))))))
    66         end;
    67 
    68     val _ =
    69       Session.init do_output false
    70         (Options.bool options "browser_info") browser_info
    71         (Options.string options "document")
    72         (Options.bool options "document_graph")
    73         (space_explode ":" (Options.string options "document_variants"))
    74         parent_name name
    75         (Options.string options "document_dump",
    76           Present.dump_mode (Options.string options "document_dump_mode"))
    77         "" verbose;
    78     val _ = Session.with_timing name verbose (List.app use_theories) theories;
    79     val _ = Session.finish ();
    80     val _ = if do_output then () else quit ();
    81   in () end
    82   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    83 
    84 end;
    85 
    86 end;