--- 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 *)
--- 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 */
--- 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;
--- 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)): _*)
}