17 (Options.set_default (Options.decode (YXML.parse_body options_yxml)); |
17 (Options.set_default (Options.decode (YXML.parse_body options_yxml)); |
18 Isabelle_Process.init_options_interactive ())); |
18 Isabelle_Process.init_options_interactive ())); |
19 |
19 |
20 val _ = |
20 val _ = |
21 Isabelle_Process.protocol_command "Prover.init_session_base" |
21 Isabelle_Process.protocol_command "Prover.init_session_base" |
22 (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml, |
22 (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml, |
23 known_theories_yxml] => |
23 loaded_theories_yxml, known_theories_yxml] => |
24 let |
24 let |
25 val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; |
25 val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; |
26 val decode_list = YXML.parse_body #> let open XML.Decode in list string end; |
26 val decode_list = YXML.parse_body #> let open XML.Decode in list string end; |
27 val decode_sessions = |
27 val decode_sessions = |
28 YXML.parse_body #> let open XML.Decode in list (pair string properties) end; |
28 YXML.parse_body #> let open XML.Decode in list (pair string properties) end; |
29 in |
29 in |
30 Resources.init_session_base |
30 Resources.init_session_base |
31 {sessions = decode_sessions sessions_yxml, |
31 {session_positions = decode_sessions session_positions_yxml, |
|
32 session_directories = decode_table session_directories_yxml, |
32 docs = decode_list doc_names_yxml, |
33 docs = decode_list doc_names_yxml, |
33 global_theories = decode_table global_theories_yxml, |
34 global_theories = decode_table global_theories_yxml, |
34 loaded_theories = decode_list loaded_theories_yxml, |
35 loaded_theories = decode_list loaded_theories_yxml, |
35 known_theories = decode_table known_theories_yxml} |
36 known_theories = decode_table known_theories_yxml} |
36 end); |
37 end); |