src/Pure/System/build.ML
author wenzelm
Tue Aug 14 15:42:58 2012 +0200 (2012-08-14)
changeset 48805 c3ea910b3581
parent 48804 6348e5fca42e
child 48927 ef462b5558eb
permissions -rw-r--r--
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
     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 = Command_Line.tool (fn () =>
    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 document_variants =
    69         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
    70       val _ =
    71         (case duplicates (op =) (map fst document_variants) of
    72           [] => ()
    73         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
    74       val _ =
    75         Session.init do_output false
    76           (Options.bool options "browser_info") browser_info
    77           (Options.string options "document")
    78           (Options.bool options "document_graph")
    79           (Options.string options "document_output")
    80           document_variants
    81           parent_name name
    82           (Options.string options "document_dump",
    83             Present.dump_mode (Options.string options "document_dump_mode"))
    84           "" verbose;
    85       val _ =
    86         theories |>
    87           (List.app use_theories
    88             |> Session.with_timing name verbose
    89             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads"));
    90 
    91       val _ = Session.finish ();
    92       val _ = if do_output then () else exit 0;
    93     in 0 end);
    94 
    95 end;
    96 
    97 end;