global session_base for PIDE interaction;
authorwenzelm
Wed Apr 12 21:13:43 2017 +0200 (2017-04-12)
changeset 65470a0f49174dbeb
parent 65469 78ace4a14975
child 65471 05e5bffcf1d8
global session_base for PIDE interaction;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/protocol.ML	Wed Apr 12 19:56:47 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Apr 12 21:13:43 2017 +0200
     1.3 @@ -18,6 +18,19 @@
     1.4         Isabelle_Process.init_options_interactive ()));
     1.5  
     1.6  val _ =
     1.7 +  Isabelle_Process.protocol_command "Prover.session_base"
     1.8 +    (fn [default_qualifier, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     1.9 +      let
    1.10 +        val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
    1.11 +      in
    1.12 +        Resources.set_session_base
    1.13 +          {default_qualifier = default_qualifier,
    1.14 +           global_theories = decode_table global_theories_yxml,
    1.15 +           loaded_theories = decode_table loaded_theories_yxml,
    1.16 +           known_theories = decode_table known_theories_yxml}
    1.17 +      end);
    1.18 +
    1.19 +val _ =
    1.20    Isabelle_Process.protocol_command "Document.define_blob"
    1.21      (fn [digest, content] => Document.change_state (Document.define_blob digest content));
    1.22  
     2.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 12 19:56:47 2017 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 12 21:13:43 2017 +0200
     2.3 @@ -302,6 +302,22 @@
     2.4      protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
     2.5  
     2.6  
     2.7 +  /* session base */
     2.8 +
     2.9 +  private def encode_table(table: List[(String, String)]): String =
    2.10 +  {
    2.11 +    import XML.Encode._
    2.12 +    Symbol.encode_yxml(list(pair(string, string))(table))
    2.13 +  }
    2.14 +
    2.15 +  def session_base(resources: Resources): Unit =
    2.16 +    protocol_command("Prover.session_base",
    2.17 +      Symbol.encode(resources.default_qualifier),
    2.18 +      encode_table(resources.session_base.global_theories.toList),
    2.19 +      encode_table(resources.session_base.dest_loaded_theories),
    2.20 +      encode_table(resources.session_base.dest_known_theories))
    2.21 +
    2.22 +
    2.23    /* interned items */
    2.24  
    2.25    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     3.1 --- a/src/Pure/PIDE/session.scala	Wed Apr 12 19:56:47 2017 +0200
     3.2 +++ b/src/Pure/PIDE/session.scala	Wed Apr 12 21:13:43 2017 +0200
     3.3 @@ -443,6 +443,7 @@
     3.4  
     3.5              case _ if output.is_init =>
     3.6                prover.get.options(session_options)
     3.7 +              prover.get.session_base(resources)
     3.8                phase = Session.Ready
     3.9                debugger.ready()
    3.10