clarified protocol messages: explicitly use physical_writeln, always encode_lines;

--- a/src/Pure/PIDE/protocol_message.ML	Sun Mar 29 12:30:27 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.ML	Sun Mar 29 13:25:59 2020 +0200
@@ -6,7 +6,8 @@
 
 signature PROTOCOL_MESSAGE =
 sig
-  val inline: string -> Properties.T -> unit
+  val inline_text: string -> string -> unit
+  val inline_properties: string -> Properties.T -> unit
   val command_positions: string -> XML.body -> XML.body
   val command_positions_yxml: string -> string -> string
 end;
@@ -14,8 +15,11 @@
 structure Protocol_Message: PROTOCOL_MESSAGE =
 struct
 
-fun inline a args =
-  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
+fun inline_text a text =
+  Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text);
+
+fun inline_properties a props =
+  inline_text a (YXML.string_of_body (XML.Encode.properties props));
 
 
 fun command_positions id =

--- a/src/Pure/Thy/export.ML	Sun Mar 29 12:30:27 2020 +0200
+++ b/src/Pure/Thy/export.ML	Sun Mar 29 13:25:59 2020 +0200
@@ -83,7 +83,10 @@
         let
           val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
           val _ = YXML.write_body path body;
-        in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
+        in
+          Protocol_Message.inline_properties (#2 function)
+            (tl args @ [(Markup.fileN, Path.implode path)])
+        end
       else raise Output.Protocol_Message props
   | [] => raise Output.Protocol_Message props);
 

--- a/src/Pure/Tools/build.ML	Sun Mar 29 12:30:27 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun Mar 29 13:25:59 2020 +0200
@@ -58,7 +58,7 @@
 
     val timing_props =
       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
-    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
+    val _ = Protocol_Message.inline_properties "Timing" timing_props;
     val _ =
       if verbose then
         Output.physical_stderr ("Timing " ^ name ^ " (" ^
@@ -73,7 +73,7 @@
   (case props of
     function :: args =>
       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
-        Protocol_Message.inline (#2 function) args
+        Protocol_Message.inline_properties (#2 function) args
       else if function = Markup.command_timing then
         let
           val name = the_default "" (Properties.get args Markup.nameN);
@@ -86,15 +86,16 @@
           if is_significant then
             (case approximative_id name pos of
               SOME id =>
-                Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed)
+                Protocol_Message.inline_properties (#2 function)
+                  (Markup.command_timing_properties id elapsed)
             | NONE => ())
           else ()
         end
       else if function = Markup.theory_timing then
-        Protocol_Message.inline (#2 function) args
+        Protocol_Message.inline_properties (#2 function) args
       else
         (case Markup.dest_loading_theory props of
-          SOME name => writeln ("\floading_theory = " ^ name)
+          SOME name => Protocol_Message.inline_text "loading_theory" name
         | NONE => Export.protocol_message props output)
   | [] => raise Output.Protocol_Message props);
 
@@ -221,7 +222,7 @@
 
 fun inline_errors exn =
   Runtime.exn_message_list exn
-  |> List.app (fn msg => writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg)));
+  |> List.app (fn msg => Protocol_Message.inline_text "error_message" (YXML.content_of msg));
 
 (*command-line tool*)
 fun build args_file =