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

diff -r 7a6301d01199 -r 4879d0021185 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sat Jun 25 09:50:40 2022 +0000
+++ b/src/Pure/PIDE/protocol.ML	Tue Jun 28 11:24:59 2022 +0200
@@ -24,7 +24,7 @@
        Isabelle_Process.init_options_interactive ()));
 
 val _ =
-  Protocol_Command.define "Prover.init_session"
+  Protocol_Command.define_bytes "Prover.init_session"
     (fn [yxml] => Resources.init_session_yxml yxml);
 
 val _ =
diff -r 7a6301d01199 -r 4879d0021185 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Jun 25 09:50:40 2022 +0000
+++ b/src/Pure/PIDE/resources.ML	Tue Jun 28 11:24:59 2022 +0200
@@ -16,7 +16,7 @@
      scala_functions: (string * ((bool * bool) * Position.T)) list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
-  val init_session_yxml: string -> unit
+  val init_session_yxml: Bytes.T -> unit
   val init_session_env: unit -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
@@ -130,7 +130,7 @@
   let
     val (session_positions, (session_directories, (bibtex_entries, (command_timings,
         (load_commands, (scala_functions, (global_theories, loaded_theories))))))) =
-      YXML.parse_body yxml |>
+      YXML.parse_body_bytes yxml |>
         let open XML.Decode in
           (pair (list (pair string properties))
             (pair (list (pair string string))
@@ -155,7 +155,7 @@
   (case getenv "ISABELLE_INIT_SESSION" of
     "" => ()
   | name =>
-      try File.read (Path.explode name)
+      try Bytes.read (Path.explode name)
       |> Option.app init_session_yxml);
 
 val _ = init_session_env ();
diff -r 7a6301d01199 -r 4879d0021185 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Jun 25 09:50:40 2022 +0000
+++ b/src/Pure/PIDE/yxml.ML	Tue Jun 28 11:24:59 2022 +0200
@@ -29,7 +29,9 @@
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
+  val parse_body_bytes: Bytes.T -> XML.body
   val parse: string -> XML.tree
+  val parse_bytes: Bytes.T -> XML.tree
   val content_of: string -> string
   val is_wellformed: string -> bool
 end;
@@ -119,6 +121,11 @@
   Substring.tokens (fn c => c = X_char) #>
   map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
 
+val split_bytes =
+  Bytes.space_explode X
+  #> filter (fn "" => false | _ => true)
+  #> map (space_explode Y);
+
 
 (* structural errors *)
 
@@ -152,19 +159,25 @@
   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
   | parse_chunk txts = fold (add o XML.Text) txts;
 
-in
-
-fun parse_body source =
-  (case fold parse_chunk (split_string source) [(("", []), [])] of
+fun parse_body' chunks =
+  (case fold parse_chunk chunks [(("", []), [])] of
     [(("", _), result)] => rev result
   | ((name, _), _) :: _ => err_unbalanced name);
 
-fun parse source =
-  (case parse_body source of
+fun parse' chunks =
+  (case parse_body' chunks of
     [result] => result
   | [] => XML.Text ""
   | _ => err "multiple results");
 
+in
+
+val parse_body = parse_body' o split_string;
+val parse_body_bytes = parse_body' o split_bytes;
+
+val parse = parse' o split_string;
+val parse_bytes = parse' o split_bytes;
+
 end;
 
 val content_of = parse_body #> XML.content_of;
diff -r 7a6301d01199 -r 4879d0021185 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Sat Jun 25 09:50:40 2022 +0000
+++ b/src/Pure/System/options.ML	Tue Jun 28 11:24:59 2022 +0200
@@ -211,8 +211,8 @@
   (case getenv "ISABELLE_PROCESS_OPTIONS" of
     "" => ()
   | name =>
-      try File.read (Path.explode name)
-      |> Option.app (set_default o decode o YXML.parse_body));
+      try Bytes.read (Path.explode name)
+      |> Option.app (set_default o decode o YXML.parse_body_bytes));
 
 val _ = load_default ();
 val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
diff -r 7a6301d01199 -r 4879d0021185 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Jun 25 09:50:40 2022 +0000
+++ b/src/Pure/Tools/build.ML	Tue Jun 28 11:24:59 2022 +0200
@@ -66,12 +66,12 @@
 (* build session *)
 
 val _ =
-  Protocol_Command.define "build_session"
+  Protocol_Command.define_bytes "build_session"
     (fn [resources_yxml, args_yxml] =>
         let
           val _ = Resources.init_session_yxml resources_yxml;
           val (session_name, theories) =
-            YXML.parse_body args_yxml |>
+            YXML.parse_body_bytes args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;