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 [XML.Text (commas ids)]; |
65 fun commands_accepted ids = |
|
66 Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; |
66 |
67 |
67 val _ = |
68 val _ = |
68 Isabelle_Process.protocol_command "Document.define_command" |
69 Isabelle_Process.protocol_command "Document.define_command" |
69 (fn id :: name :: blobs :: toks :: sources => |
70 (fn id :: name :: blobs :: toks :: sources => |
70 let |
71 let |