--- a/src/Pure/PIDE/protocol.ML Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML Tue Nov 17 22:05:59 2020 +0100
@@ -25,27 +25,7 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session"
- (fn [html_symbols_yxml, session_positions_yxml, session_directories_yxml, session_chapters_yxml,
- bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
- let
- val decode_symbols = YXML.parse_body #> let open XML.Decode in list (pair string int) end;
- 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;
- val decode_bibtex_entries =
- YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end;
- in
- Resources.init_session
- {html_symbols = decode_symbols html_symbols_yxml,
- session_positions = decode_sessions session_positions_yxml,
- session_directories = decode_table session_directories_yxml,
- session_chapters = decode_table session_chapters_yxml,
- bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
- docs = decode_list doc_names_yxml,
- global_theories = decode_table global_theories_yxml,
- loaded_theories = decode_list loaded_theories_yxml}
- end);
+ (fn [yxml] => Resources.init_session_yxml yxml);
val _ =
Isabelle_Process.protocol_command "Document.define_blob"