29 |
29 |
30 val _ = |
30 val _ = |
31 Isabelle_Process.protocol_command "Document.define_blob" |
31 Isabelle_Process.protocol_command "Document.define_blob" |
32 (fn [digest, content] => Document.change_state (Document.define_blob digest content)); |
32 (fn [digest, content] => Document.change_state (Document.define_blob digest content)); |
33 |
33 |
34 fun decode_command id name blobs_xml toks_xml sources : Document.command = |
34 fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command = |
35 let |
35 let |
36 open XML.Decode; |
36 open XML.Decode; |
|
37 val parents = list string parents_xml; |
37 val (blobs_digests, blobs_index) = |
38 val (blobs_digests, blobs_index) = |
38 blobs_xml |> |
39 blobs_xml |> |
39 let |
40 let |
40 val message = YXML.string_of_body o Protocol_Message.command_positions id; |
41 val message = YXML.string_of_body o Protocol_Message.command_positions id; |
41 val blob = |
42 val blob = |
50 end; |
51 end; |
51 val toks = list (pair int int) toks_xml; |
52 val toks = list (pair int int) toks_xml; |
52 in |
53 in |
53 {command_id = Document_ID.parse id, |
54 {command_id = Document_ID.parse id, |
54 name = name, |
55 name = name, |
|
56 parents = parents, |
55 blobs_digests = blobs_digests, |
57 blobs_digests = blobs_digests, |
56 blobs_index = blobs_index, |
58 blobs_index = blobs_index, |
57 tokens = toks ~~ sources} |
59 tokens = toks ~~ sources} |
58 end; |
60 end; |
59 |
61 |
60 fun commands_accepted ids = |
62 fun commands_accepted ids = |
61 Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; |
63 Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; |
62 |
64 |
63 val _ = |
65 val _ = |
64 Isabelle_Process.protocol_command "Document.define_command" |
66 Isabelle_Process.protocol_command "Document.define_command" |
65 (fn id :: name :: blobs :: toks :: sources => |
67 (fn id :: name :: parents :: blobs :: toks :: sources => |
66 let |
68 let |
67 val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; |
69 val command = |
|
70 decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs) |
|
71 (YXML.parse_body toks) sources; |
68 val _ = Document.change_state (Document.define_command command); |
72 val _ = Document.change_state (Document.define_command command); |
69 in commands_accepted [id] end); |
73 in commands_accepted [id] end); |
70 |
74 |
71 val _ = |
75 val _ = |
72 Isabelle_Process.protocol_command "Document.define_commands" |
76 Isabelle_Process.protocol_command "Document.define_commands" |
73 (fn args => |
77 (fn args => |
74 let |
78 let |
75 fun decode arg = |
79 fun decode arg = |
76 let |
80 let |
77 open XML.Decode; |
81 open XML.Decode; |
78 val (id, (name, (blobs_xml, (toks_xml, sources)))) = |
82 val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) = |
79 pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); |
83 pair string (pair string (pair I (pair I (pair I (list string))))) |
80 in decode_command id name blobs_xml toks_xml sources end; |
84 (YXML.parse_body arg); |
|
85 in decode_command id name parents_xml blobs_xml toks_xml sources end; |
81 |
86 |
82 val commands = map decode args; |
87 val commands = map decode args; |
83 val _ = Document.change_state (fold Document.define_command commands); |
88 val _ = Document.change_state (fold Document.define_command commands); |
84 in commands_accepted (map (Value.print_int o #command_id) commands) end); |
89 in commands_accepted (map (Value.print_int o #command_id) commands) end); |
85 |
90 |