# HG changeset patch
# User wenzelm
# Date 1585510340 -7200
# Node ID ab5009192ebb3db936e06329a46e0bb7df05e468
# Parent  281591ab169bcccfd1f30f732e3f08c28e7bffb2
tuned signature -- follow Scala;

diff -r 281591ab169b -r ab5009192ebb src/Pure/PIDE/protocol_message.ML
--- a/src/Pure/PIDE/protocol_message.ML	Sun Mar 29 19:47:42 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.ML	Sun Mar 29 21:32:20 2020 +0200
@@ -6,8 +6,8 @@
 
 signature PROTOCOL_MESSAGE =
 sig
-  val inline_text: string -> string -> unit
-  val inline_properties: string -> Properties.T -> unit
+  val marker_text: string -> string -> unit
+  val marker: string -> Properties.T -> unit
   val command_positions: string -> XML.body -> XML.body
   val command_positions_yxml: string -> string -> string
 end;
@@ -15,11 +15,11 @@
 structure Protocol_Message: PROTOCOL_MESSAGE =
 struct
 
-fun inline_text a text =
+fun marker_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 marker a props =
+  marker_text a (YXML.string_of_body (XML.Encode.properties props));
 
 
 fun command_positions id =
diff -r 281591ab169b -r ab5009192ebb src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Sun Mar 29 19:47:42 2020 +0200
+++ b/src/Pure/Thy/export.ML	Sun Mar 29 21:32:20 2020 +0200
@@ -83,10 +83,7 @@
         let
           val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
           val _ = YXML.write_body path body;
-        in
-          Protocol_Message.inline_properties (#2 function)
-            (tl args @ [(Markup.fileN, Path.implode path)])
-        end
+        in Protocol_Message.marker (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
       else raise Output.Protocol_Message props
   | [] => raise Output.Protocol_Message props);
 
diff -r 281591ab169b -r ab5009192ebb src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun Mar 29 19:47:42 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun Mar 29 21:32:20 2020 +0200
@@ -58,7 +58,7 @@
 
     val timing_props =
       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
-    val _ = Protocol_Message.inline_properties "Timing" timing_props;
+    val _ = Protocol_Message.marker "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_properties (#2 function) args
+        Protocol_Message.marker (#2 function) args
       else if function = Markup.command_timing then
         let
           val name = the_default "" (Properties.get args Markup.nameN);
@@ -86,16 +86,16 @@
           if is_significant then
             (case approximative_id name pos of
               SOME id =>
-                Protocol_Message.inline_properties (#2 function)
+                Protocol_Message.marker (#2 function)
                   (Markup.command_timing_properties id elapsed)
             | NONE => ())
           else ()
         end
       else if function = Markup.theory_timing then
-        Protocol_Message.inline_properties (#2 function) args
+        Protocol_Message.marker (#2 function) args
       else
         (case Markup.dest_loading_theory props of
-          SOME name => Protocol_Message.inline_text "loading_theory" name
+          SOME name => Protocol_Message.marker_text "loading_theory" name
         | NONE => Export.protocol_message props output)
   | [] => raise Output.Protocol_Message props);
 
@@ -222,7 +222,7 @@
 
 fun inline_errors exn =
   Runtime.exn_message_list exn
-  |> List.app (fn msg => Protocol_Message.inline_text "error_message" (YXML.content_of msg));
+  |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg));
 
 (*command-line tool*)
 fun build args_file =