--- 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) +
--- 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,
--- 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),
--- 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 _ =>
--- 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()
--- 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,