--- 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 */
--- 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
--- a/src/Pure/PIDE/session.scala Sun Mar 29 21:57:40 2020 +0200
+++ b/src/Pure/PIDE/session.scala Sun Mar 29 22:23:33 2020 +0200
@@ -486,7 +486,7 @@
case Protocol.Theory_Timing(_, _) =>
// FIXME
- case Markup.Export(args)
+ case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
val id = Value.Long.unapply(args.id.get).get
val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
--- a/src/Pure/Thy/export.scala Sun Mar 29 21:57:40 2020 +0200
+++ b/src/Pure/Thy/export.scala Sun Mar 29 22:23:33 2020 +0200
@@ -143,7 +143,7 @@
regex.pattern.matcher(compound_name(theory_name, name)).matches
}
- def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
+ def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes,
cache: XZ.Cache = XZ.cache()): Entry =
{
Entry(session_name, args.theory_name, args.name, args.executable,
@@ -213,7 +213,7 @@
(results, true)
})
- def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
+ def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit =
consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict)
def shutdown(close: Boolean = false): List[String] =
--- a/src/Pure/Tools/build.scala Sun Mar 29 21:57:40 2020 +0200
+++ b/src/Pure/Tools/build.scala Sun Mar 29 22:23:33 2020 +0200
@@ -296,7 +296,7 @@
line match {
case Loading_Theory_Marker(theory) =>
progress.theory(Progress.Theory(theory, session = name))
- case Markup.Export.Marker((args, path)) =>
+ case Protocol.Export.Marker((args, path)) =>
val body =
try { Bytes.read(path) }
catch {