# HG changeset patch
# User wenzelm
# Date 1590309402 -7200
# Node ID aaa984499d361703cb2f3fb2470544e70396cd4d
# Parent  9d31fe4ecaea637a7197104d2f827b8d1bd545b7
tuned signature;

diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun May 24 10:36:42 2020 +0200
@@ -92,7 +92,7 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
-          List("Resources.init_session_base" +
+          List("Resources.init_session" +
             " {session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", docs = " + print_list(base.doc_names) +
diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML	Sun May 24 10:36:42 2020 +0200
@@ -18,7 +18,7 @@
        Isabelle_Process.init_options_interactive ()));
 
 val _ =
-  Isabelle_Process.protocol_command "Prover.init_session_base"
+  Isabelle_Process.protocol_command "Prover.init_session"
     (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
           loaded_theories_yxml] =>
       let
@@ -27,7 +27,7 @@
         val decode_sessions =
           YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
       in
-        Resources.init_session_base
+        Resources.init_session
           {session_positions = decode_sessions session_positions_yxml,
            session_directories = decode_table session_directories_yxml,
            docs = decode_list doc_names_yxml,
diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sun May 24 10:36:42 2020 +0200
@@ -328,9 +328,9 @@
     Symbol.encode_yxml(list(pair(string, properties))(lst))
   }
 
-  def session_base(resources: Resources)
+  def init_session(resources: Resources)
   {
-    protocol_command("Prover.init_session_base",
+    protocol_command("Prover.init_session",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
       encode_list(resources.session_base.doc_names),
diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Sun May 24 10:36:42 2020 +0200
@@ -7,7 +7,7 @@
 signature RESOURCES =
 sig
   val default_qualifier: string
-  val init_session_base:
+  val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
      docs: string list,
@@ -61,7 +61,7 @@
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base
+fun init_session
     {session_positions, session_directories, docs, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Sun May 24 10:36:42 2020 +0200
@@ -548,7 +548,7 @@
 
             case _ if output.is_init =>
               prover.get.options(file_formats.prover_options(session_options))
-              prover.get.session_base(resources)
+              prover.get.init_session(resources)
               phase = Session.Ready
               debugger.ready()
 
diff -r 9d31fe4ecaea -r aaa984499d36 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 24 10:36:42 2020 +0200
@@ -184,7 +184,7 @@
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
-      Resources.init_session_base
+      Resources.init_session
         {session_positions = session_positions,
          session_directories = session_directories,
          docs = doc_names,