# HG changeset patch
# User wenzelm
# Date 1585513413 -7200
# Node ID f0499449e149fa117d8adc6434a444ab2edd2b9e
# Parent  b3bddebe44caeb4f7cc87e5bc29a816fd3b9869d
clarified modules;

diff -r b3bddebe44ca -r f0499449e149 src/Pure/PIDE/markup.scala
--- 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 */
diff -r b3bddebe44ca -r f0499449e149 src/Pure/PIDE/protocol.scala
--- 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
diff -r b3bddebe44ca -r f0499449e149 src/Pure/PIDE/session.scala
--- 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)
diff -r b3bddebe44ca -r f0499449e149 src/Pure/Thy/export.scala
--- 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] =
diff -r b3bddebe44ca -r f0499449e149 src/Pure/Tools/build.scala
--- 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 {