proper protocol_message for bootstrap proofs;

--- a/src/Pure/General/output.ML	Sat Oct 19 11:29:39 2019 +0200
+++ b/src/Pure/General/output.ML	Sat Oct 19 11:33:36 2019 +0200
@@ -29,6 +29,7 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
+  val protocol_message_undefined: Properties.T -> string list -> unit
   val writelns: string list -> unit
   val state: string -> unit
   val information: string -> unit
@@ -120,6 +121,9 @@
 
 exception Protocol_Message of Properties.T;
 
+fun protocol_message_undefined props (_: string list) =
+  raise Protocol_Message props;
+
 fun init_channels () =
  (writeln_fn := (physical_writeln o implode);
   state_fn := (fn ss => ! writeln_fn ss);
@@ -132,7 +136,7 @@
   status_fn := Output_Primitives.ignore_outputs;
   report_fn := Output_Primitives.ignore_outputs;
   result_fn := (fn _ => Output_Primitives.ignore_outputs);
-  protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
+  protocol_message_fn := protocol_message_undefined);
 
 val _ = if Thread_Data.is_virtual then () else init_channels ();
 

--- a/src/Pure/PIDE/protocol_message.ML	Sat Oct 19 11:29:39 2019 +0200
+++ b/src/Pure/PIDE/protocol_message.ML	Sat Oct 19 11:33:36 2019 +0200
@@ -6,6 +6,7 @@
 
 signature PROTOCOL_MESSAGE =
 sig
+  val inline: string -> Properties.T -> unit
   val command_positions: string -> XML.body -> XML.body
   val command_positions_yxml: string -> string -> string
 end;
@@ -13,6 +14,10 @@
 structure Protocol_Message: PROTOCOL_MESSAGE =
 struct
 
+fun inline a args =
+  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
+
+
 fun command_positions id =
   let
     fun attribute (a, b) =

--- a/src/Pure/ROOT.ML	Sat Oct 19 11:29:39 2019 +0200
+++ b/src/Pure/ROOT.ML	Sat Oct 19 11:33:36 2019 +0200
@@ -90,6 +90,7 @@
 
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/yxml.ML";
+ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 
 ML_file "General/change_table.ML";
@@ -314,7 +315,6 @@
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
-ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document.ML";
 
 (*theory and proof operations*)

--- a/src/Pure/Thy/export.ML	Sat Oct 19 11:29:39 2019 +0200
+++ b/src/Pure/Thy/export.ML	Sat Oct 19 11:33:36 2019 +0200
@@ -16,6 +16,7 @@
   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
 end;
 
 structure Export: EXPORT =
@@ -67,4 +68,24 @@
 fun message thy path =
   "See " ^ Markup.markup (markup thy path) "theory exports";
 
+
+(* protocol message (bootstrap) *)
+
+fun protocol_message props output =
+  (case props of
+    function :: args =>
+      if function = (Markup.functionN, Markup.exportN) andalso
+        not (null args) andalso #1 (hd args) = Markup.idN
+      then
+        let
+          val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
+          val _ = File.write_list path output;
+        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);
+
+val _ =
+  if Thread_Data.is_virtual then ()
+  else Private_Output.protocol_message_fn := protocol_message;
+
 end;

--- a/src/Pure/Tools/build.ML	Sat Oct 19 11:29:39 2019 +0200
+++ b/src/Pure/Tools/build.ML	Sat Oct 19 11:33:36 2019 +0200
@@ -69,14 +69,11 @@
 
 (* protocol messages *)
 
-fun inline_message a args =
-  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
-
 fun protocol_message props output =
   (case props of
     function :: args =>
       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
-        inline_message (#2 function) args
+        Protocol_Message.inline (#2 function) args
       else if function = Markup.command_timing then
         let
           val name = the_default "" (Properties.get args Markup.nameN);
@@ -88,23 +85,17 @@
         in
           if is_significant then
             (case approximative_id name pos of
-              SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
+              SOME id =>
+                Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed)
             | NONE => ())
           else ()
         end
       else if function = Markup.theory_timing then
-        inline_message (#2 function) args
-      else if function = (Markup.functionN, Markup.exportN) andalso
-        not (null args) andalso #1 (hd args) = Markup.idN
-      then
-        let
-          val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
-          val _ = File.write_list path output;
-        in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
+        Protocol_Message.inline (#2 function) args
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
-        | NONE => raise Output.Protocol_Message props)
+        | NONE => Export.protocol_message props output)
   | [] => raise Output.Protocol_Message props);
 
 
@@ -240,6 +231,7 @@
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
         build_session args
       handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
+    val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined;
     val _ = Options.reset_default ();
   in () end;