--- a/src/Pure/Tools/build.ML Wed Jan 14 16:23:33 2015 +0100
+++ b/src/Pure/Tools/build.ML Wed Jan 14 16:27:19 2015 +0100
@@ -97,6 +97,28 @@
(* build *)
+fun build_theories last_timing master_dir (options, thys) =
+ let
+ val condition = space_explode "," (Options.string options "condition");
+ val conds = filter_out (can getenv_strict) condition;
+ in
+ if null conds then
+ (Options.set_default options;
+ (Thy_Info.use_theories {
+ document = Present.document_enabled (Options.string options "document"),
+ last_timing = last_timing,
+ master_dir = master_dir}
+ |> Unsynchronized.setmp print_mode
+ (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+ |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+ |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+ |> Multithreading.max_threads_setmp (Options.int options "threads")
+ |> Unsynchronized.setmp Future.ML_statistics true) thys)
+ else
+ Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
+ " (undefined " ^ commas conds ^ ")\n")
+ end;
+
fun build args_file = Command_Line.tool0 (fn () =>
let
val _ = SHA1_Samples.test ();
@@ -129,7 +151,7 @@
val res1 =
theories |>
- (List.app (Thy_Info.build_theories last_timing Path.current)
+ (List.app (build_theories last_timing Path.current)
|> session_timing name verbose
|> Unsynchronized.setmp Output.protocol_message_fn protocol_message
|> Multithreading.max_threads_setmp (Options.int options "threads")
@@ -141,4 +163,24 @@
val _ = if do_output then () else exit 0;
in () end);
+
+(* PIDE protocol *)
+
+val _ =
+ Isabelle_Process.protocol_command "build_theories"
+ (fn [id, master_dir, theories_yxml] =>
+ let
+ val theories =
+ YXML.parse_body theories_yxml |>
+ let open XML.Decode
+ in list (pair Options.decode (list (string #> rpair Position.none))) end;
+ val result =
+ Exn.capture (fn () =>
+ theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
+ val ok =
+ (case result of
+ Exn.Res _ => true
+ | Exn.Exn exn => (Runtime.exn_error_message exn; false));
+ in Output.protocol_message (Markup.build_theories_result id ok) [] end);
+
end;