src/Pure/Tools/build.ML
author wenzelm
Tue Mar 12 16:47:24 2013 +0100 (2013-03-12 ago)
changeset 51399 6ac3c29a300e
parent 51398 c3d02b3518c2
child 51423 e5f9a6d9ca82
permissions -rw-r--r--
discontinued "isabelle usedir" option -r (reset session path);
simplified internal session identification: chapter / name;
clarified chapter index (of sessions) vs. session index (of theories);
discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser);
removed obsolete session parent_path;
     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 local
    18 
    19 (* FIXME avoid hardwired stuff!? *)
    20 val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    21 
    22 fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
    23 
    24 in
    25 
    26 fun protocol_message props output =
    27   (case props of
    28     function :: args =>
    29       if member (op =) protocol_echo function then
    30         writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    31       else
    32         (case Markup.dest_loading_theory props of
    33           SOME name => writeln ("\floading_theory = " ^ name)
    34         | NONE => protocol_undef ())
    35   | [] => protocol_undef ());
    36 
    37 end;
    38 
    39 
    40 (* build *)
    41 
    42 local
    43 
    44 fun no_document options =
    45   (case Options.string options "document" of "" => true | "false" => true | _ => false);
    46 
    47 fun use_theories last_timing options =
    48   Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    49     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    50     |> Unsynchronized.setmp print_mode
    51         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    52     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    53     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    54         (Options.int options "parallel_proofs_threshold")
    55     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    56     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    57     |> Unsynchronized.setmp Future.ML_statistics true
    58     |> no_document options ? Present.no_document
    59     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    60     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    61     |> Unsynchronized.setmp Printer.show_question_marks_default
    62         (Options.bool options "show_question_marks")
    63     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    64     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    65     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    66     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    67     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    68     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    69     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    70     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    71     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    72     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    73 
    74 fun use_theories_condition last_timing (options, thys) =
    75   let val condition = space_explode "," (Options.string options "condition") in
    76     (case filter_out (can getenv_strict) condition of
    77       [] => use_theories last_timing options (map (rpair Position.none) thys)
    78     | conds =>
    79         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    80           " (undefined " ^ commas conds ^ ")\n"))
    81   end;
    82 
    83 
    84 (* command timings *)
    85 
    86 type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
    87 
    88 val empty_timings: timings = Symtab.empty;
    89 
    90 fun update_timings props =
    91   (case Markup.parse_command_timing_properties props of
    92     SOME ({file, offset, name}, time) =>
    93       Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
    94   | NONE => I);
    95 
    96 fun lookup_timings timings tr =
    97   (case Toplevel.approximative_id tr of
    98     SOME {file, offset, name} =>
    99       (case Symtab.lookup timings file of
   100         SOME offsets =>
   101           (case Inttab.lookup offsets offset of
   102             SOME (name', time) => if name = name' then time else Time.zeroTime
   103           | NONE => Time.zeroTime)
   104       | NONE => Time.zeroTime)
   105   | NONE => Time.zeroTime);
   106 
   107 in
   108 
   109 fun build args_file = Command_Line.tool (fn () =>
   110     let
   111       val (command_timings, (do_output, (options, (verbose, (browser_info,
   112           (parent_name, (chapter, (name, theories)))))))) =
   113         File.read (Path.explode args_file) |> YXML.parse_body |>
   114           let open XML.Decode in
   115             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   116               (pair string (pair string (pair string
   117                 ((list (pair Options.decode (list string)))))))))))
   118           end;
   119 
   120       val document_variants =
   121         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   122       val _ =
   123         (case duplicates (op =) (map fst document_variants) of
   124           [] => ()
   125         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   126 
   127       val _ = writeln ("\fSession.name = " ^ name);
   128       val _ =
   129         Session.init do_output
   130           (Options.bool options "browser_info")
   131           (Path.explode browser_info)
   132           (Options.string options "document")
   133           (Options.bool options "document_graph")
   134           (Options.string options "document_output")
   135           document_variants
   136           parent_name (chapter, name)
   137           (false, "")
   138           verbose;
   139 
   140       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   141 
   142       val res1 =
   143         theories |>
   144           (List.app (use_theories_condition last_timing)
   145             |> Session.with_timing name verbose
   146             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   147             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   148             |> Exn.capture);
   149       val res2 = Exn.capture Session.finish ();
   150       val _ = Par_Exn.release_all [res1, res2];
   151 
   152       val _ = if do_output then () else exit 0;
   153     in 0 end);
   154 
   155 end;
   156 
   157 end;