equal
deleted
inserted
replaced
60 blobs_digests = blobs_digests, |
60 blobs_digests = blobs_digests, |
61 blobs_index = blobs_index, |
61 blobs_index = blobs_index, |
62 tokens = toks ~~ sources} |
62 tokens = toks ~~ sources} |
63 end; |
63 end; |
64 |
64 |
|
65 fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids]; |
|
66 |
65 val _ = |
67 val _ = |
66 Isabelle_Process.protocol_command "Document.define_command" |
68 Isabelle_Process.protocol_command "Document.define_command" |
67 (fn id :: name :: blobs :: toks :: sources => |
69 (fn id :: name :: blobs :: toks :: sources => |
68 let |
70 let |
69 val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; |
71 val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; |
70 in Document.change_state (Document.define_command command) end); |
72 val _ = Document.change_state (Document.define_command command); |
|
73 in commands_accepted [id] end); |
71 |
74 |
72 val _ = |
75 val _ = |
73 Isabelle_Process.protocol_command "Document.define_commands" |
76 Isabelle_Process.protocol_command "Document.define_commands" |
74 (fn args => |
77 (fn args => |
75 let |
78 let |
77 let |
80 let |
78 open XML.Decode; |
81 open XML.Decode; |
79 val (id, (name, (blobs_xml, (toks_xml, sources)))) = |
82 val (id, (name, (blobs_xml, (toks_xml, sources)))) = |
80 pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); |
83 pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); |
81 in decode_command id name blobs_xml toks_xml sources end; |
84 in decode_command id name blobs_xml toks_xml sources end; |
82 in Document.change_state (fold (Document.define_command o decode) args) end); |
85 |
|
86 val commands = map decode args; |
|
87 val _ = Document.change_state (fold Document.define_command commands); |
|
88 in commands_accepted (map (Value.print_int o #command_id) commands) end); |
83 |
89 |
84 val _ = |
90 val _ = |
85 Isabelle_Process.protocol_command "Document.discontinue_execution" |
91 Isabelle_Process.protocol_command "Document.discontinue_execution" |
86 (fn [] => Execution.discontinue ()); |
92 (fn [] => Execution.discontinue ()); |
87 |
93 |