src/Pure/PIDE/protocol.ML

--- a/src/Pure/PIDE/protocol.ML	Sun Apr 11 21:32:09 2021 +0200
+++ b/src/Pure/PIDE/protocol.ML	Sun Apr 11 22:47:55 2021 +0200
@@ -60,7 +60,7 @@
   end;
 
 fun commands_accepted ids =
-  Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)];
+  Output.protocol_message Markup.commands_accepted [[XML.Text (space_implode "," ids)]];
 
 val _ =
   Protocol_Command.define "Document.define_command"
@@ -141,12 +141,12 @@
 
             val _ =
               Output.protocol_message Markup.assign_update
-                ((new_id, edited, assign_update) |>
+                [(new_id, edited, assign_update) |>
                   let
                     open XML.Encode;
                     fun encode_upd (a, bs) =
                       string (space_implode "," (map Value.print_int (a :: bs)));
-                  in triple int (list string) (list encode_upd) end);
+                  in triple int (list string) (list encode_upd) end];
           in Document.start_execution state' end)));
 
 val _ =
@@ -157,7 +157,7 @@
           YXML.parse_body versions_yxml |>
             let open XML.Decode in list int end;
         val state1 = Document.remove_versions versions state;
-        val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)];
+        val _ = Output.protocol_message Markup.removed_versions [[XML.Text (versions_yxml)]];
       in state1 end));
 
 val _ =