# HG changeset patch
# User wenzelm
# Date 1606135934 -3600
# Node ID 2126cf9460866686d19f15dfb2224af5d755ad3d
# Parent  53064415757a941f48f6483774839f4a00c405c4
clarified signature;

diff -r 53064415757a -r 2126cf946086 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Nov 23 13:37:10 2020 +0100
+++ b/src/Pure/Thy/export.scala	Mon Nov 23 13:52:14 2020 +0100
@@ -13,7 +13,13 @@
 
 object Export
 {
-  /* name structure */
+  /* artefact names */
+
+  val MARKUP = "markup.yxml"
+  val MESSAGES = "messages.yxml"
+  val DOCUMENT_PREFIX = "document/"
+  val THEORY_PREFIX: String = "theory/"
+  val PROOFS_PREFIX: String = "proofs/"
 
   def explode_name(s: String): List[String] = space_explode('/', s)
   def implode_name(elems: Iterable[String]): String = elems.mkString("/")
@@ -89,6 +95,7 @@
 
     def compound_name: String = Export.compound_name(theory_name, name)
 
+    def name_has_prefix(s: String): Boolean = name.startsWith(s)
     val name_elems: List[String] = explode_name(name)
 
     def name_extends(elems: List[String]): Boolean =
diff -r 53064415757a -r 2126cf946086 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Nov 23 13:37:10 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala	Mon Nov 23 13:52:14 2020 +0100
@@ -62,9 +62,6 @@
 
   /** theory content **/
 
-  val export_prefix: String = "theory/"
-  val export_prefix_proofs: String = "proofs/"
-
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
@@ -115,7 +112,7 @@
     val parents =
       if (theory_name == Thy_Header.PURE) Nil
       else {
-        provider(export_prefix + "parents") match {
+        provider(Export.THEORY_PREFIX + "parents") match {
           case Some(entry) => split_lines(entry.uncompressed().text)
           case None =>
             error("Missing theory export in session " + quote(session_name) + ": " +
@@ -239,7 +236,7 @@
   }
 
   def read_types(provider: Export.Provider): List[Type] =
-    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.TYPE, tree)
         val (syntax, args, abbrev) =
@@ -271,7 +268,7 @@
   }
 
   def read_consts(provider: Export.Provider): List[Const] =
-    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CONST, tree)
         val (syntax, (typargs, (typ, (abbrev, propositional)))) =
@@ -318,7 +315,7 @@
   }
 
   def read_axioms(provider: Export.Provider): List[Axiom] =
-    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "axioms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.AXIOM, tree)
         val prop = decode_prop(body)
@@ -348,7 +345,7 @@
   }
 
   def read_thms(provider: Export.Provider): List[Thm] =
-    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.THM, tree)
         val (prop, deps, prf) =
@@ -379,7 +376,7 @@
   def read_proof(
     provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
   {
-    for { entry <- provider.focus(id.theory_name)(export_prefix_proofs + id.serial) }
+    for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
     yield {
       val body = entry.uncompressed_yxml()
       val (typargs, (args, (prop_body, proof_body))) =
@@ -454,7 +451,7 @@
   }
 
   def read_classes(provider: Export.Provider): List[Class] =
-    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "classes").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CLASS, tree)
         val (params, axioms) =
@@ -483,7 +480,7 @@
   }
 
   def read_locales(provider: Export.Provider): List[Locale] =
-    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "locales").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.LOCALE, tree)
         val (typargs, args, axioms) =
@@ -520,7 +517,7 @@
   }
 
   def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
-    provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "locale_dependencies").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
         val (source, (target, (prefix, (subst_types, subst_terms)))) =
@@ -544,7 +541,7 @@
 
   def read_classrel(provider: Export.Provider): List[Classrel] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "classrel")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
     val classrel =
     {
       import XML.Decode._
@@ -562,7 +559,7 @@
 
   def read_arities(provider: Export.Provider): List[Arity] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "arities")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
     val arities =
     {
       import XML.Decode._
@@ -583,7 +580,7 @@
 
   def read_constdefs(provider: Export.Provider): List[Constdef] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "constdefs")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
     val constdefs =
     {
       import XML.Decode._
@@ -609,7 +606,7 @@
 
   def read_typedefs(provider: Export.Provider): List[Typedef] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
     val typedefs =
     {
       import XML.Decode._
@@ -645,7 +642,7 @@
 
   def read_datatypes(provider: Export.Provider): List[Datatype] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "datatypes")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
     val datatypes =
     {
       import XML.Decode._
@@ -741,7 +738,7 @@
 
   def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
     val spec_rules =
     {
       import XML.Decode._
diff -r 53064415757a -r 2126cf946086 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Nov 23 13:37:10 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Nov 23 13:52:14 2020 +0100
@@ -49,25 +49,26 @@
     List(
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
-            args.write(Path.explode("markup.yxml"),
+            args.write(Path.explode(Export.MARKUP),
               args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
         }),
       Aspect("messages", "output messages (YXML format)",
         { case args =>
-            args.write(Path.explode("messages.yxml"),
+            args.write(Path.explode(Export.MESSAGES),
               args.snapshot.messages.iterator.map(_._1).toList)
         }),
       Aspect("latex", "generated LaTeX source",
         { case args =>
-            for (entry <- args.snapshot.exports if entry.name.startsWith("document/")) {
-              args.write(Path.explode(entry.name), entry.uncompressed())
-            }
+            for {
+              entry <- args.snapshot.exports
+              if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
+            } args.write(Path.explode(entry.name), entry.uncompressed())
         }),
       Aspect("theory", "foundational theory content",
         { case args =>
             for {
               entry <- args.snapshot.exports
-              if entry.name.startsWith(Export_Theory.export_prefix)
+              if entry.name_has_prefix(Export.THEORY_PREFIX)
             } args.write(Path.explode(entry.name), entry.uncompressed())
         }, options = List("export_theory"))
     ).sortBy(_.name)