diff -r ab5009192ebb -r b3bddebe44ca src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Mar 29 21:32:20 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sun Mar 29 21:57:40 2020 +0200
@@ -184,6 +184,8 @@
 
   /* job: running prover process */
 
+  private val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
+
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
@@ -291,24 +293,19 @@
 
           process.result(
             progress_stdout = (line: String) =>
-              Library.try_unprefix("\floading_theory = ", line) match {
-                case Some(theory) =>
+              line match {
+                case Loading_Theory_Marker(theory) =>
                   progress.theory(Progress.Theory(theory, session = name))
-                case None =>
-                  for {
-                    text <- Library.try_unprefix("\fexport = ", line)
-                    (args, path) <-
-                      Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
-                  } {
-                    val body =
-                      try { Bytes.read(path) }
-                      catch {
-                        case ERROR(msg) =>
-                          error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
-                      }
-                    path.file.delete
-                    export_consumer(name, args, body)
-                  }
+                case Markup.Export.Marker((args, path)) =>
+                  val body =
+                    try { Bytes.read(path) }
+                    catch {
+                      case ERROR(msg) =>
+                        error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
+                    }
+                  path.file.delete
+                  export_consumer(name, args, body)
+                case _ =>
               },
             progress_limit =
               options.int("process_output_limit") match {
@@ -540,7 +537,7 @@
 
             val (process_result, heap_digest) = job.join
 
-            val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
+            val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail =
             {
               val tail = job.info.options.int("process_output_tail")