src/Pure/Tools/build.ML
author wenzelm
Thu Jan 03 20:42:18 2013 +0100 (2013-01-03 ago)
changeset 50707 5b2bf7611662
parent 50698 49621c755075
child 50777 20126dd9772c
permissions -rw-r--r--
maintain session index on Scala side, for more determistic results;
removed unused HTML operations;
     1 (*  Title:      Pure/Tools/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 (* protocol messages *)
    16 
    17 fun ML_statistics (function :: stats) "" =
    18       if function = Markup.ML_statistics then SOME stats
    19       else NONE
    20   | ML_statistics _ _ = NONE;
    21 
    22 fun protocol_message props output =
    23   (case ML_statistics props output of
    24     SOME stats =>
    25       writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
    26   | NONE => raise Fail "Undefined Output.protocol_message");
    27 
    28 
    29 (* build *)
    30 
    31 local
    32 
    33 fun no_document options =
    34   (case Options.string options "document" of "" => true | "false" => true | _ => false);
    35 
    36 fun use_thys options =
    37   Thy_Info.use_thys
    38     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    39     |> Unsynchronized.setmp print_mode
    40         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    41     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    42     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    43         (Options.int options "parallel_proofs_threshold")
    44     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    45     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    46     |> Unsynchronized.setmp Future.ML_statistics true
    47     |> no_document options ? Present.no_document
    48     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    49     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    50     |> Unsynchronized.setmp Printer.show_question_marks_default
    51         (Options.bool options "show_question_marks")
    52     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    53     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    54     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    55     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    56     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    57     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    58     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    59     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    60     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    61     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    62 
    63 fun use_theories (options, thys) =
    64   let val condition = space_explode "," (Options.string options "condition") in
    65     (case filter_out (can getenv_strict) condition of
    66       [] => use_thys options (map (rpair Position.none) thys)
    67     | conds =>
    68         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    69           " (undefined " ^ commas conds ^ ")\n"))
    70   end;
    71 
    72 in
    73 
    74 fun build args_file = Command_Line.tool (fn () =>
    75     let
    76       val (do_output, (options, (verbose, (browser_info, (parent_name,
    77           (name, theories)))))) =
    78         File.read (Path.explode args_file) |> YXML.parse_body |>
    79           let open XML.Decode in
    80             pair bool (pair Options.decode (pair bool (pair string (pair string
    81               (pair string ((list (pair Options.decode (list string)))))))))
    82           end;
    83 
    84       val document_variants =
    85         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
    86       val _ =
    87         (case duplicates (op =) (map fst document_variants) of
    88           [] => ()
    89         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
    90 
    91       val _ =
    92         (case Session.path () of
    93           [] => ()
    94         | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
    95       val _ =
    96         Session.init do_output false
    97           (Options.bool options "browser_info") browser_info
    98           (Options.string options "document")
    99           (Options.bool options "document_graph")
   100           (Options.string options "document_output")
   101           document_variants
   102           parent_name name
   103           (false, "") ""
   104           verbose;
   105 
   106       val res1 =
   107         theories |>
   108           (List.app use_theories
   109             |> Session.with_timing name verbose
   110             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   111             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   112             |> Exn.capture);
   113       val res2 = Exn.capture Session.finish ();
   114       val _ = Par_Exn.release_all [res1, res2];
   115 
   116       val _ = if do_output then () else exit 0;
   117     in 0 end);
   118 
   119 end;
   120 
   121 end;