37 |
37 |
38 val _ = |
38 val _ = |
39 Isabelle_Process.protocol_command "Document.define_blob" |
39 Isabelle_Process.protocol_command "Document.define_blob" |
40 (fn [digest, content] => Document.change_state (Document.define_blob digest content)); |
40 (fn [digest, content] => Document.change_state (Document.define_blob digest content)); |
41 |
41 |
42 fun decode_command id name blobs_yxml toks_yxml sources : Document.command = |
42 fun decode_command id name blobs_xml toks_xml sources : Document.command = |
43 let |
43 let |
44 open XML.Decode; |
44 open XML.Decode; |
45 val (blobs_digests, blobs_index) = |
45 val (blobs_digests, blobs_index) = |
46 YXML.parse_body blobs_yxml |> |
46 blobs_xml |> |
47 let |
47 let |
48 val message = YXML.string_of_body o Protocol_Message.command_positions id; |
48 val message = YXML.string_of_body o Protocol_Message.command_positions id; |
49 in |
49 in |
50 pair |
50 pair |
51 (list (variant |
51 (list (variant |
52 [fn ([], a) => Exn.Res (pair string (option string) a), |
52 [fn ([], a) => Exn.Res (pair string (option string) a), |
53 fn ([], a) => Exn.Exn (ERROR (message a))])) |
53 fn ([], a) => Exn.Exn (ERROR (message a))])) |
54 int |
54 int |
55 end; |
55 end; |
56 val toks = YXML.parse_body toks_yxml |> list (pair int int); |
56 val toks = list (pair int int) toks_xml; |
57 in |
57 in |
58 {command_id = Document_ID.parse id, |
58 {command_id = Document_ID.parse id, |
59 name = name, |
59 name = name, |
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 val _ = |
65 val _ = |
66 Isabelle_Process.protocol_command "Document.define_command" |
66 Isabelle_Process.protocol_command "Document.define_command" |
67 (fn id :: name :: blobs_yxml :: toks_yxml :: sources => |
67 (fn id :: name :: blobs :: toks :: sources => |
68 Document.change_state |
68 let |
69 (Document.define_command (decode_command id name blobs_yxml toks_yxml sources))); |
69 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); |
|
71 |
|
72 val _ = |
|
73 Isabelle_Process.protocol_command "Document.define_commands" |
|
74 (fn args => |
|
75 let |
|
76 fun decode arg = |
|
77 let |
|
78 open XML.Decode; |
|
79 val (id, (name, (blobs_xml, (toks_xml, sources)))) = |
|
80 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; |
|
82 in Document.change_state (fold (Document.define_command o decode) args) end); |
70 |
83 |
71 val _ = |
84 val _ = |
72 Isabelle_Process.protocol_command "Document.discontinue_execution" |
85 Isabelle_Process.protocol_command "Document.discontinue_execution" |
73 (fn [] => Execution.discontinue ()); |
86 (fn [] => Execution.discontinue ()); |
74 |
87 |