# HG changeset patch
# User wenzelm
# Date 1397733696 -7200
# Node ID abc2da18d08db9617eebc9596b192b9aa50efb7a
# Parent  47c1dbeec36a17fc96cdf5af08a890dea7a5c112
added protocol command "use_theories", with core functionality of batch build;

diff -r 47c1dbeec36a -r abc2da18d08d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Apr 17 12:03:15 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Apr 17 13:21:36 2014 +0200
@@ -184,6 +184,7 @@
   val command_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
+  val use_theories_result: string -> bool -> Properties.T
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
@@ -580,6 +581,9 @@
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   | dest_loading_theory _ = NONE;
 
+fun use_theories_result id ok =
+  [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
+
 
 (* simplifier trace *)
 
diff -r 47c1dbeec36a -r abc2da18d08d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Apr 17 12:03:15 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Apr 17 13:21:36 2014 +0200
@@ -420,6 +420,25 @@
       }
   }
 
+  object Loading_Theory
+  {
+    def unapply(props: Properties.T): Option[String] =
+      props match {
+        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
+        case _ => None
+      }
+  }
+
+  object Use_Theories_Result
+  {
+    def unapply(props: Properties.T): Option[(String, Boolean)] =
+      props match {
+        case List((FUNCTION, "use_theories_result"),
+          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
+        case _ => None
+      }
+  }
+
 
   /* simplifier trace */
 
diff -r 47c1dbeec36a -r abc2da18d08d src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Apr 17 12:03:15 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Apr 17 13:21:36 2014 +0200
@@ -108,5 +108,20 @@
       Active.dialog_result (Markup.parse_int serial) result
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
 
+val _ =
+  Isabelle_Process.protocol_command "use_theories"
+    (fn id :: master_dir :: thys =>
+      let
+        val result =
+          Exn.capture (fn () =>
+            Thy_Info.use_theories
+              {document = false, last_timing = K NONE, master_dir = Path.explode master_dir}
+              (map (rpair Position.none) thys)) ();
+        val ok =
+          (case result of
+            Exn.Res _ => true
+          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
+    in Output.protocol_message (Markup.use_theories_result id ok) [] end);
+
 end;
 
diff -r 47c1dbeec36a -r abc2da18d08d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Apr 17 12:03:15 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Apr 17 13:21:36 2014 +0200
@@ -428,4 +428,10 @@
 
   def dialog_result(serial: Long, result: String): Unit =
     protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
+
+
+  /* use_theories */
+
+  def use_theories(id: String, master_dir: Path, thys: List[Path]): Unit =
+    protocol_command("use_theories", (id :: master_dir.implode :: thys.map(_.implode)): _*)
 }