diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/Tools/build.ML
--- 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;