--- a/src/Pure/PIDE/protocol.ML Wed Apr 12 19:56:47 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed Apr 12 21:13:43 2017 +0200
@@ -18,6 +18,19 @@
Isabelle_Process.init_options_interactive ()));
val _ =
+ Isabelle_Process.protocol_command "Prover.session_base"
+ (fn [default_qualifier, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
+ let
+ val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
+ in
+ Resources.set_session_base
+ {default_qualifier = default_qualifier,
+ global_theories = decode_table global_theories_yxml,
+ loaded_theories = decode_table loaded_theories_yxml,
+ known_theories = decode_table known_theories_yxml}
+ end);
+
+val _ =
Isabelle_Process.protocol_command "Document.define_blob"
(fn [digest, content] => Document.change_state (Document.define_blob digest content));
--- a/src/Pure/PIDE/protocol.scala Wed Apr 12 19:56:47 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Apr 12 21:13:43 2017 +0200
@@ -302,6 +302,22 @@
protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
+ /* session base */
+
+ private def encode_table(table: List[(String, String)]): String =
+ {
+ import XML.Encode._
+ Symbol.encode_yxml(list(pair(string, string))(table))
+ }
+
+ def session_base(resources: Resources): Unit =
+ protocol_command("Prover.session_base",
+ Symbol.encode(resources.default_qualifier),
+ encode_table(resources.session_base.global_theories.toList),
+ encode_table(resources.session_base.dest_loaded_theories),
+ encode_table(resources.session_base.dest_known_theories))
+
+
/* interned items */
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
--- a/src/Pure/PIDE/session.scala Wed Apr 12 19:56:47 2017 +0200
+++ b/src/Pure/PIDE/session.scala Wed Apr 12 21:13:43 2017 +0200
@@ -443,6 +443,7 @@
case _ if output.is_init =>
prover.get.options(session_options)
+ prover.get.session_base(resources)
phase = Session.Ready
debugger.ready()