unused (see also 7b318273a4aa);

--- a/src/Pure/PIDE/protocol.scala	Tue Sep 01 16:57:54 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Sep 01 17:51:20 2020 +0200
@@ -12,7 +12,6 @@
   /* markers for inlined messages */
 
   val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
-  val Export_Marker = Protocol_Message.Marker("export")
   val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
   val Command_Timing_Marker = Protocol_Message.Marker("command_timing")
   val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing")
@@ -200,30 +199,6 @@
       def compound_name: String = isabelle.Export.compound_name(theory_name, name)
     }
 
-    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(
-                  (Markup.SERIAL, Value.Long(serial)),
-                  (Markup.THEORY_NAME, theory_name),
-                  (Markup.NAME, name),
-                  (Markup.EXECUTABLE, Value.Boolean(executable)),
-                  (Markup.COMPRESS, Value.Boolean(compress)),
-                  (Markup.STRICT, Value.Boolean(strict)),
-                  (Markup.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