# HG changeset patch
# User wenzelm
# Date 1492024423 -7200
# Node ID a0f49174dbebf5ac97b1c51aef5add51311798bf
# Parent  78ace4a1497560841691f670fd762975c8b01537
global session_base for PIDE interaction;

diff -r 78ace4a14975 -r a0f49174dbeb src/Pure/PIDE/protocol.ML
--- 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));
 
diff -r 78ace4a14975 -r a0f49174dbeb src/Pure/PIDE/protocol.scala
--- 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 =
diff -r 78ace4a14975 -r a0f49174dbeb src/Pure/PIDE/session.scala
--- 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()