src/Pure/PIDE/protocol.scala

   {
     val text = Pretty.string_of(List(msg))
     if (is_warning(msg) || is_legacy(msg)) Library.prefix_lines("### ", text)
     else if (is_error(msg)) Library.prefix_lines("*** ", text)
     else text
+  }
+
+
+  /* export */
+
+  val Export_Marker = Protocol_Message.Marker(Markup.EXPORT)
+
+  object Export
+  {
+    sealed case class Args(
+      id: Option[String],
+      serial: Long,
+      theory_name: String,
+      name: String,
+      executable: Boolean,
+      compress: Boolean,
+      strict: Boolean)
+    {
+      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
+          List(
+            (Markup.FUNCTION, Markup.EXPORT),
+            (Markup.ID, id),
+            (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))) =>
+          Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict))
+        case _ => None
+      }
   }
 
 
   /* breakpoints */