--- a/src/Pure/PIDE/protocol.ML Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/PIDE/protocol.ML Tue Jan 23 19:25:39 2018 +0100
@@ -24,10 +24,12 @@
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;
+ val decode_sessions =
+ YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
in
Resources.init_session_base
- {sessions = decode_list sessions_yxml,
- doc_names = decode_list doc_names_yxml,
+ {sessions = decode_sessions sessions_yxml,
+ docs = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
loaded_theories = decode_list loaded_theories_yxml,
known_theories = decode_table known_theories_yxml}