--- a/src/Pure/PIDE/protocol.ML Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/PIDE/protocol.ML Sat Dec 16 21:53:07 2017 +0100
@@ -18,14 +18,15 @@
Isabelle_Process.init_options_interactive ()));
val _ =
- Isabelle_Process.protocol_command "Prover.session_base"
- (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
+ Isabelle_Process.protocol_command "Prover.init_session_base"
+ (fn [sessions_yxml, 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;
val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
in
Resources.init_session_base
- {global_theories = decode_table global_theories_yxml,
+ {sessions = decode_list sessions_yxml,
+ global_theories = decode_table global_theories_yxml,
loaded_theories = decode_list loaded_theories_yxml,
known_theories = decode_table known_theories_yxml}
end);