--- a/src/Pure/PIDE/protocol.scala Sun Mar 29 21:57:40 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala Sun Mar 29 22:23:33 2020 +0200
@@ -159,6 +159,66 @@
}
+ /* 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 */
object ML_Breakpoint