src/Pure/Thy/export.ML

   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: Output.protocol_message_fn
 end;
 
 structure Export: EXPORT =
 struct
 

   in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
 
 fun message thy path =
   "See " ^ Markup.markup (markup thy path) "theory exports";
 
-
-(* protocol message (bootstrap) *)
-
-fun protocol_message props body =
-  (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 _ = YXML.write_body path body;
-        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);
-
-val _ =
-  if Thread_Data.is_virtual then ()
-  else Private_Output.protocol_message_fn := protocol_message;
-
 end;