equal
deleted
inserted
replaced
20 val _ = |
20 val _ = |
21 Isabelle_Process.protocol_command "Prover.session_base" |
21 Isabelle_Process.protocol_command "Prover.session_base" |
22 (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] => |
22 (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] => |
23 let |
23 let |
24 val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; |
24 val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; |
|
25 val decode_list = YXML.parse_body #> let open XML.Decode in list string end; |
25 in |
26 in |
26 Resources.init_session_base |
27 Resources.init_session_base |
27 {global_theories = decode_table global_theories_yxml, |
28 {global_theories = decode_table global_theories_yxml, |
28 loaded_theories = decode_table loaded_theories_yxml, |
29 loaded_theories = decode_list loaded_theories_yxml, |
29 known_theories = decode_table known_theories_yxml} |
30 known_theories = decode_table known_theories_yxml} |
30 end); |
31 end); |
31 |
32 |
32 val _ = |
33 val _ = |
33 Isabelle_Process.protocol_command "Document.define_blob" |
34 Isabelle_Process.protocol_command "Document.define_blob" |