clarified signature: more explicit type Protocol_Message.Marker;

--- a/src/Pure/PIDE/markup.scala	Sun Mar 29 21:32:20 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Mar 29 21:57:40 2020 +0200
@@ -625,6 +625,7 @@
   /* export */
 
   val EXPORT = "export"
+  val Export_Marker = Protocol_Message.Marker(EXPORT)
 
   object Export
   {
@@ -645,25 +646,34 @@
     val COMPRESS = "compress"
     val STRICT = "strict"
 
-    def dest_inline(props: Properties.T): Option[(Args, Path)] =
+    object Marker
+    {
+      def unapply(line: String): Option[(Args, Path)] =
+        line match {
+          case Export_Marker(text) =>
+            val props = XML.Decode.properties(YXML.parse_body(text))
+            props match {
+              case
+                List(
+                  (SERIAL, Value.Long(serial)),
+                  (THEORY_NAME, theory_name),
+                  (NAME, name),
+                  (EXECUTABLE, Value.Boolean(executable)),
+                  (COMPRESS, Value.Boolean(compress)),
+                  (STRICT, Value.Boolean(strict)),
+                  (FILE, file)) if isabelle.Path.is_valid(file) =>
+                val args = Args(None, serial, theory_name, name, executable, compress, strict)
+                Some((args, isabelle.Path.explode(file)))
+              case _ => None
+            }
+          case _ => None
+        }
+    }
+
+    def unapply(props: Properties.T): Option[Args] =
       props match {
         case
           List(
-            (SERIAL, Value.Long(serial)),
-            (THEORY_NAME, theory_name),
-            (NAME, name),
-            (EXECUTABLE, Value.Boolean(executable)),
-            (COMPRESS, Value.Boolean(compress)),
-            (STRICT, Value.Boolean(strict)),
-            (FILE, file)) if isabelle.Path.is_valid(file) =>
-          val args = Args(None, serial, theory_name, name, executable, compress, strict)
-          Some((args, isabelle.Path.explode(file)))
-        case _ => None
-      }
-
-    def unapply(props: Properties.T): Option[Args] =
-      props match {
-        case List(
             (FUNCTION, EXPORT),
             (ID, id),
             (SERIAL, Value.Long(serial)),

--- a/src/Pure/PIDE/protocol_message.scala	Sun Mar 29 21:32:20 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Sun Mar 29 21:57:40 2020 +0200
@@ -15,6 +15,8 @@
   {
     def apply(a: String): Marker =
       new Marker { override def name: String = a }
+
+    def test(line: String): Boolean = line.startsWith("\f")
   }
 
   abstract class Marker private

--- 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")