# HG changeset patch
# User wenzelm
# Date 1656420659 -7200
# Node ID c8263ac985e1fb5fe6708d8637e032669603354a
# Parent  4879d00211858a25d5c45626a89edb3b2c961c7a
more operations on Bytes.T;

diff -r 4879d0021185 -r c8263ac985e1 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Tue Jun 28 11:24:59 2022 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Jun 28 14:50:59 2022 +0200
@@ -18,9 +18,9 @@
        raise Protocol_Command.STOP (Value.parse_int rc)));
 
 val _ =
-  Protocol_Command.define "Prover.options"
+  Protocol_Command.define_bytes "Prover.options"
     (fn [options_yxml] =>
-      (Options.set_default (Options.decode (YXML.parse_body options_yxml));
+      (Options.set_default (Options.decode (YXML.parse_body_bytes options_yxml));
        Isabelle_Process.init_options_interactive ()));
 
 val _ =
@@ -97,18 +97,18 @@
     (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
 
 val _ =
-  Protocol_Command.define "Document.update"
+  Protocol_Command.define_bytes "Document.update"
     (Future.task_context "Document.update" (Future.new_group NONE)
-      (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
+      (fn old_id_bytes :: new_id_bytes :: consolidate_yxml :: edits_yxml =>
         Document.change_state (fn state =>
           let
-            val old_id = Document_ID.parse old_id_string;
-            val new_id = Document_ID.parse new_id_string;
+            val old_id = Document_ID.parse (Bytes.content old_id_bytes);
+            val new_id = Document_ID.parse (Bytes.content new_id_bytes);
             val consolidate =
-              YXML.parse_body consolidate_yxml |>
+              YXML.parse_body_bytes consolidate_yxml |>
                 let open XML.Decode in list string end;
             val edits =
-              edits_yxml |> map (YXML.parse_body #>
+              edits_yxml |> map (YXML.parse_body_bytes #>
                 let open XML.Decode in
                   pair string
                     (variant
@@ -151,14 +151,14 @@
           in Document.start_execution state' end)));
 
 val _ =
-  Protocol_Command.define "Document.remove_versions"
+  Protocol_Command.define_bytes "Document.remove_versions"
     (fn [versions_yxml] => Document.change_state (fn state =>
       let
         val versions =
-          YXML.parse_body versions_yxml |>
+          YXML.parse_body_bytes 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 [Bytes.contents_blob versions_yxml];
       in state1 end));
 
 val _ =