# HG changeset patch # User wenzelm # Date 1585481159 -7200 # Node ID e33f6e5f86b679c28eef47a3cf0a9fb5424c9e90 # Parent 1b8861bcb03c0c5ade4cfa1761caed91855fc7df clarified protocol messages: explicitly use physical_writeln, always encode_lines; diff -r 1b8861bcb03c -r e33f6e5f86b6 src/Pure/PIDE/protocol_message.ML --- 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 = diff -r 1b8861bcb03c -r e33f6e5f86b6 src/Pure/Thy/export.ML --- 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); diff -r 1b8861bcb03c -r e33f6e5f86b6 src/Pure/Tools/build.ML --- 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 =