src/Pure/PIDE/markup.scala

 
 
   /* export */
 
   val EXPORT = "export"
-  val Export_Marker = Protocol_Message.Marker(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)
-    }
-
-    val THEORY_NAME = "theory_name"
-    val EXECUTABLE = "executable"
-    val COMPRESS = "compress"
-    val STRICT = "strict"
-
-    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(
-            (FUNCTION, EXPORT),
-            (ID, id),
-            (SERIAL, Value.Long(serial)),
-            (THEORY_NAME, theory_name),
-            (NAME, name),
-            (EXECUTABLE, Value.Boolean(executable)),
-            (COMPRESS, Value.Boolean(compress)),
-            (STRICT, Value.Boolean(strict))) =>
-          Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict))
-        case _ => None
-      }
-  }
+  val THEORY_NAME = "theory_name"
+  val EXECUTABLE = "executable"
+  val COMPRESS = "compress"
+  val STRICT = "strict"
 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"