# HG changeset patch
# User wenzelm
# Date 1572692547 -3600
# Node ID f9f7c34b7dd48f450f2841afb2bbced7521ce91c
# Parent  e5e34bd28257ee532bbc79e8154d20d7426f0de0
more scalable protocol_message: use XML.body directly (Output.output hook is not required);

diff -r e5e34bd28257 -r f9f7c34b7dd4 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -973,8 +973,8 @@
           val prv_path = Path.ext "prv" path;
           val _ =
             Export.export thy (Path.binding (prv_path, Position.none))
-              [implode (map (fn (s, _) => snd (strip_number s) ^
-                " -- proved by " ^ Distribution.version ^ "\n") proved'')];
+              (proved'' |> map (fn (s, _) =>
+                XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n")));
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))
   |> Sign.parent_path;
 
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/General/output.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -28,8 +28,9 @@
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
+  type protocol_message_fn = Output_Primitives.protocol_message_fn
   exception Protocol_Message of Properties.T
-  val protocol_message_undefined: Properties.T -> string list -> unit
+  val protocol_message_undefined: protocol_message_fn
   val writelns: string list -> unit
   val state: string -> unit
   val information: string -> unit
@@ -39,8 +40,8 @@
   val status: string list -> unit
   val report: string list -> unit
   val result: Properties.T -> string list -> unit
-  val protocol_message: Properties.T -> string list -> unit
-  val try_protocol_message: Properties.T -> string list -> unit
+  val protocol_message: protocol_message_fn
+  val try_protocol_message: protocol_message_fn
 end;
 
 signature PRIVATE_OUTPUT =
@@ -57,7 +58,7 @@
   val status_fn: (output list -> unit) Unsynchronized.ref
   val report_fn: (output list -> unit) Unsynchronized.ref
   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
-  val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
+  val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
   val init_channels: unit -> unit
 end;
 
@@ -105,6 +106,8 @@
 val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
 val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
 val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
+
+type protocol_message_fn = Output_Primitives.protocol_message_fn;
 val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
 
 
@@ -121,8 +124,8 @@
 
 exception Protocol_Message of Properties.T;
 
-fun protocol_message_undefined props (_: string list) =
-  raise Protocol_Message props;
+val protocol_message_undefined: Output_Primitives.protocol_message_fn =
+  fn props => fn _ => raise Protocol_Message props;
 
 fun init_channels () =
  (writeln_fn := (physical_writeln o implode);
@@ -153,8 +156,8 @@
 fun status ss = ! status_fn (map output ss);
 fun report ss = ! report_fn (map output ss);
 fun result props ss = ! result_fn props (map output ss);
-fun protocol_message props ss = ! protocol_message_fn props (map output ss);
-fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
+fun protocol_message props body = ! protocol_message_fn props body;
+fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
 
 
 (* profiling *)
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/General/output_primitives.ML
--- a/src/Pure/General/output_primitives.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/General/output_primitives.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -6,6 +6,14 @@
 
 signature OUTPUT_PRIMITIVES =
 sig
+  structure XML:
+  sig
+    type attributes = (string * string) list
+    datatype tree =
+        Elem of (string * attributes) * tree list
+      | Text of string
+    type body = tree list
+  end
   type output = string
   type serial = int
   type properties = (string * string) list
@@ -21,13 +29,31 @@
   val status_fn: output list -> unit
   val report_fn: output list -> unit
   val result_fn: properties -> output list -> unit
-  val protocol_message_fn: properties -> output list -> unit
+  type protocol_message_fn = properties -> XML.body -> unit
+  val protocol_message_fn: protocol_message_fn
   val markup_fn: string * properties -> output * output
 end;
 
 structure Output_Primitives: OUTPUT_PRIMITIVES =
 struct
 
+(** XML trees **)
+
+structure XML =
+struct
+
+type attributes = (string * string) list;
+
+datatype tree =
+    Elem of (string * attributes) * tree list
+  | Text of string;
+
+type body = tree list;
+end;
+
+
+(* output *)
+
 type output = string;
 type serial = int;
 type properties = (string * string) list;
@@ -45,7 +71,9 @@
 val status_fn = ignore_outputs;
 val report_fn = ignore_outputs;
 fun result_fn (_: properties) = ignore_outputs;
-fun protocol_message_fn (_: properties) = ignore_outputs;
+
+type protocol_message_fn = properties -> XML.body -> unit;
+val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
 
 fun markup_fn (_: string * properties) = ("", "");
 
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -62,7 +62,7 @@
     tokens = toks ~~ sources}
   end;
 
-fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids];
+fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (commas ids)];
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
@@ -146,8 +146,7 @@
                     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
-                  |> YXML.chunks_of_body);
+                  in triple int (list string) (list encode_upd) end);
           in Document.start_execution state' end)));
 
 val _ =
@@ -158,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 [versions_yxml];
+        val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)];
       in state1 end));
 
 val _ =
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -34,6 +34,7 @@
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
+  val blob: string list -> body
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
@@ -73,13 +74,9 @@
 
 (** XML trees **)
 
-type attributes = (string * string) list;
+open Output_Primitives.XML;
 
-datatype tree =
-    Elem of (string * attributes) * tree list
-  | Text of string;
-
-type body = tree list;
+val blob = map Text;
 
 
 (* wrapped elements *)
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -25,6 +25,7 @@
   val chunks_of_body: XML.body -> string list
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
+  val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
@@ -81,6 +82,10 @@
 fun string_of_body body = Buffer.empty |> fold buffer body |> Buffer.content;
 val string_of = string_of_body o single;
 
+fun write_body path body =
+  path |> File.open_output (fn file =>
+    fold (traverse (fn s => fn () => BinIO.output (file, Byte.stringToBytes s))) body ());
+
 
 (* markup elements *)
 
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/System/invoke_scala.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -33,7 +33,7 @@
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
     val promise = Future.promise_name "invoke_scala" abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
-    val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
+    val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   in promise end;
 
 fun method name arg = Future.join (promise_method name arg);
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -131,7 +131,8 @@
     Private_Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     Private_Output.system_message_fn := message Markup.systemN [];
-    Private_Output.protocol_message_fn := message Markup.protocolN;
+    Private_Output.protocol_message_fn :=
+      (fn props => fn body => message Markup.protocolN props (YXML.chunks_of_body body));
 
     Session.init_protocol_handlers ();
     message Markup.initN [] [Session.welcome ()];
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Thy/export.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -9,14 +9,14 @@
   val report_export: theory -> Path.binding -> unit
   type params =
     {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
-  val export_params: params -> string list -> unit
-  val export: theory -> Path.binding -> string list -> unit
-  val export_executable: theory -> Path.binding -> string list -> unit
+  val export_params: params -> XML.body -> unit
+  val export: theory -> Path.binding -> XML.body -> unit
+  val export_executable: theory -> Path.binding -> XML.body -> unit
   val export_file: theory -> Path.binding -> Path.T -> unit
   val export_executable_file: theory -> Path.binding -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
-  val protocol_message: Properties.T -> string list -> unit
+  val protocol_message: Output.protocol_message_fn
 end;
 
 structure Export: EXPORT =
@@ -34,7 +34,7 @@
 type params =
   {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
-fun export_params ({theory = thy, binding, executable, compress, strict}: params) blob =
+fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
@@ -43,18 +43,21 @@
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
-    strict = strict} blob);
+    strict = strict} body);
 
-fun export thy binding blob =
+fun export thy binding body =
   export_params
-    {theory = thy, binding = binding, executable = false, compress = true, strict = true} blob;
+    {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
 
-fun export_executable thy binding blob =
+fun export_executable thy binding body =
   export_params
-    {theory = thy, binding = binding, executable = true, compress = true, strict = true} blob;
+    {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
 
-fun export_file thy binding file = export thy binding [File.read file];
-fun export_executable_file thy binding file = export_executable thy binding [File.read file];
+fun export_file thy binding file =
+  export thy binding [XML.Text (File.read file)];
+
+fun export_executable_file thy binding file =
+  export_executable thy binding [XML.Text (File.read file)];
 
 
 (* information message *)
@@ -71,7 +74,7 @@
 
 (* protocol message (bootstrap) *)
 
-fun protocol_message props output =
+fun protocol_message props body =
   (case props of
     function :: args =>
       if function = (Markup.functionN, Markup.exportN) andalso
@@ -79,7 +82,7 @@
       then
         let
           val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
-          val _ = File.write_list path output;
+          val _ = YXML.write_body path body;
         in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
       else raise Output.Protocol_Message props
   | [] => raise Output.Protocol_Message props);
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -127,7 +127,7 @@
 
 fun export_buffer thy name buffer =
   if Buffer.is_empty buffer then ()
-  else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer);
+  else Export.export thy (Path.binding0 (Path.make ["theory", name])) (XML.blob (Buffer.chunks buffer));
 
 fun export_body thy name body =
   export_buffer thy name (fold YXML.buffer body Buffer.empty);
@@ -420,7 +420,7 @@
 
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
-        [YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))];
+        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
 
   in () end);
 
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -65,8 +65,9 @@
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
             val _ =
-              if Options.bool options "export_document"
-              then Export.export thy (Path.explode_binding0 "document.tex") output else ();
+              if Options.bool options "export_document" then
+                Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output)
+              else ();
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Tools/build.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -239,11 +239,12 @@
 val _ =
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
-      let
-        val args = decode_args args_yxml;
-        val result = (build_session args; "") handle exn =>
-          (Runtime.exn_message exn handle _ (*sic!*) =>
-            "Exception raised, but failed to print details!");
-    in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
+        let
+          val args = decode_args args_yxml;
+          val result = (build_session args; "") handle exn =>
+            (Runtime.exn_message exn handle _ (*sic!*) =>
+              "Exception raised, but failed to print details!");
+        in Output.protocol_message Markup.build_session_finished [XML.Text result] end
+      | _ => raise Match);
 
 end;
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Tools/debugger.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -23,7 +23,7 @@
   else
     Output.protocol_message
       (Markup.debugger_output (Standard_Thread.the_name ()))
-      [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
+      [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
 
 val writeln_message = output_message Markup.writelnN;
 val warning_message = output_message Markup.warningN;
@@ -201,13 +201,12 @@
 
 fun debugger_state thread_name =
   Output.protocol_message (Markup.debugger_state thread_name)
-   [get_debugging ()
+   (get_debugging ()
     |> map (fn st =>
       (Position.properties_of
         (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
        PolyML.DebuggerInterface.debugFunction st))
-    |> let open XML.Encode in list (pair properties string) end
-    |> YXML.string_of_body];
+    |> let open XML.Encode in list (pair properties string) end);
 
 fun debugger_command thread_name =
   (case get_input thread_name of
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -136,7 +136,7 @@
   in () end;
 
 fun export_file thy (file: file) =
-  Export.export thy (file_binding file) [#content file];
+  Export.export thy (file_binding file) [XML.Text (#content file)];
 
 
 (* file types *)
@@ -290,7 +290,7 @@
                 Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
             in
               (if is_some executable then Export.export_executable else Export.export)
-                thy binding' [content]
+                thy binding' [XML.Text content]
             end));
       val _ =
         if null export then ()
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Tools/print_operation.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -23,13 +23,9 @@
 
 fun report () =
   Output.try_protocol_message Markup.print_operations
-    let
-      val yxml =
-        Synchronized.value print_operations
-        |> map (fn (x, (y, _)) => (x, y)) |> rev
-        |> let open XML.Encode in list (pair string string) end
-        |> YXML.string_of_body;
-    in [yxml] end;
+    (Synchronized.value print_operations
+      |> map (fn (x, (y, _)) => (x, y)) |> rev
+      |> let open XML.Encode in list (pair string string) end);
 
 val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
 
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/proofterm.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -2151,12 +2151,12 @@
         val encode_proof = encode_standard_proof consts;
       in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
   in
-    YXML.chunks_of_body xml |> Export.export_params
+    Export.export_params
      {theory = thy,
       binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
       executable = false,
       compress = true,
-      strict = false}
+      strict = false} xml
   end;
 
 fun export thy i prop prf =
diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -282,7 +282,7 @@
 fun export binding content thy =
   let
     val thy' = thy |> Generated_Files.add_files (binding, content);
-    val _ = Export.export thy' binding [content];
+    val _ = Export.export thy' binding [XML.Text content];
   in thy' end;
 
 local