--- a/src/Pure/PIDE/markup.scala Sun Mar 29 21:57:40 2020 +0200
+++ b/src/Pure/PIDE/markup.scala Sun Mar 29 22:23:33 2020 +0200
@@ -625,67 +625,10 @@
/* 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 */