export other entities, e.g. relevant for formal document output;
clarified markup kind (PIDE) vs. export kind (e.g. MMT);

--- a/src/Pure/General/name_space.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/General/name_space.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -9,17 +9,19 @@
 
 signature NAME_SPACE =
 sig
+  type entry =
+   {concealed: bool,
+    group: serial option,
+    theory_long_name: string,
+    pos: Position.T,
+    serial: serial}
   type T
   val empty: string -> T
   val kind_of: T -> string
   val markup: T -> string -> Markup.T
   val markup_def: T -> string -> Markup.T
-  val the_entry: T -> string ->
-   {concealed: bool,
-    group: serial option,
-    theory_long_name: string,
-    pos: Position.T,
-    serial: serial}
+  val get_names: T -> string list
+  val the_entry: T -> string -> entry
   val the_entry_theory_name: T -> string -> string
   val entry_ord: T -> string ord
   val is_concealed: T -> string -> bool
@@ -182,6 +184,9 @@
       | NONE => ("Undefined", quote bad));
   in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
 
+fun get_names (Name_Space {entries, ...}) =
+  Change_Table.fold (cons o #1) entries [];
+
 fun the_entry (space as Name_Space {entries, ...}) name =
   (case Change_Table.lookup entries name of
     NONE => error (undefined space name)

--- a/src/Pure/Isar/attrib.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -9,6 +9,7 @@
   type thms = Attrib.thms
   type fact = Attrib.fact
   val print_attributes: bool -> Proof.context -> unit
+  val attribute_space: Context.generic -> Name_Space.T
   val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory
   val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory
   val check_name_generic: Context.generic -> xstring * Position.T -> string
@@ -114,7 +115,7 @@
     |> Pretty.writeln_chunks
   end;
 
-val attribute_space = Name_Space.space_of_table o get_attributes;
+val attribute_space = Name_Space.space_of_table o Attributes.get;
 
 
 (* define *)
@@ -393,7 +394,7 @@
         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
-    val space = attribute_space ctxt;
+    val space = attribute_space (Context.Proof ctxt);
     val configs =
       Name_Space.markup_entries verbose ctxt space
         (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt)));

--- a/src/Pure/Isar/bundle.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -7,6 +7,7 @@
 signature BUNDLE =
 sig
   type name = string
+  val bundle_space: Context.generic -> Name_Space.T
   val check: Proof.context -> xstring * Position.T -> string
   val get: Proof.context -> name -> Attrib.thms
   val read: Proof.context -> xstring * Position.T -> Attrib.thms
@@ -35,7 +36,7 @@
 structure Data = Generic_Data
 (
   type T = Attrib.thms Name_Space.table * Attrib.thms option;
-  val empty : T = (Name_Space.empty_table "bundle", NONE);
+  val empty : T = (Name_Space.empty_table Markup.bundleN, NONE);
   val extend = I;
   fun merge ((tab1, target1), (tab2, target2)) =
     (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2));
@@ -49,6 +50,8 @@
 val get_all_generic = #1 o Data.get;
 val get_all = get_all_generic o Context.Proof;
 
+val bundle_space = Name_Space.space_of_table o #1 o Data.get;
+
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt);
 
 val get = Name_Space.get o get_all_generic o Context.Proof;

--- a/src/Pure/Isar/method.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -38,6 +38,7 @@
   val erule: Proof.context -> int -> thm list -> method
   val drule: Proof.context -> int -> thm list -> method
   val frule: Proof.context -> int -> thm list -> method
+  val method_space: Context.generic -> Name_Space.T
   val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
   val clean_facts: thm list -> thm list
   val set_facts: thm list -> Proof.context -> Proof.context
@@ -312,6 +313,8 @@
  {get_data = get_methods,
   put_data = fn methods => map_data (fn (_, ml_tactic, facts) => (methods, ml_tactic, facts))};
 
+val method_space = Name_Space.space_of_table o get_methods;
+
 
 (* ML tactic *)
 

--- a/src/Pure/PIDE/markup.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -91,6 +91,7 @@
   val theoryN: string
   val classN: string
   val localeN: string
+  val bundleN: string
   val type_nameN: string
   val constantN: string
   val axiomN: string
@@ -481,6 +482,7 @@
 val theoryN = "theory";
 val classN = "class";
 val localeN = "locale";
+val bundleN = "bundle";
 val type_nameN = "type_name";
 val constantN = "constant";
 val axiomN = "axiom";

--- a/src/Pure/PIDE/markup.scala	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Sep 07 21:16:22 2021 +0200
@@ -306,6 +306,7 @@
   val THEORY = "theory"
   val CLASS = "class"
   val LOCALE = "locale"
+  val BUNDLE = "bundle"
   val TYPE_NAME = "type_name"
   val CONSTANT = "constant"
   val AXIOM = "axiom"

--- a/src/Pure/Thy/export_theory.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -6,6 +6,7 @@
 
 signature EXPORT_THEORY =
 sig
+  val other_name_space: (theory -> Name_Space.T) -> theory -> theory
   val export_enabled: Thy_Info.presentation_context -> bool
   val export_body: theory -> string -> XML.body -> unit
 end;
@@ -13,6 +14,39 @@
 structure Export_Theory: EXPORT_THEORY =
 struct
 
+(* other name spaces *)
+
+fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind);
+
+structure Data = Theory_Data
+(
+  type T = ((theory -> Name_Space.T) * serial) Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  fun merge data =
+    Symtab.merge (eq_snd op =) data
+      handle Symtab.DUP dup => err_dup_kind dup;
+);
+
+val other_name_spaces = map (#1 o #2) o Symtab.dest o Data.get;
+
+fun other_name_space get_space thy =
+  let
+    val kind = Name_Space.kind_of (get_space thy);
+    val entry = (get_space, serial ());
+  in
+    Data.map (Symtab.update_new (kind, entry)) thy
+      handle Symtab.DUP dup => err_dup_kind dup
+  end;
+
+val _ = Theory.setup
+ (other_name_space Thm.oracle_space #>
+  other_name_space Global_Theory.fact_space #>
+  other_name_space (Bundle.bundle_space o Context.Theory) #>
+  other_name_space (Attrib.attribute_space o Context.Theory) #>
+  other_name_space (Method.method_space o Context.Theory));
+
+
 (* approximative syntax *)
 
 val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
@@ -115,7 +149,7 @@
 
 fun export_body thy name body =
   if XML.is_empty_body body then ()
-  else Export.export thy (Path.binding0 (Path.make ["theory", name])) body;
+  else Export.export thy (Path.binding0 (Path.make ("theory" :: space_explode "/" name))) body;
 
 val _ = (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy =>
   let
@@ -271,7 +305,7 @@
 
     fun entity_markup_thm (serial, (name, i)) =
       let
-        val space = Facts.space_of (Global_Theory.facts_of thy);
+        val space = Global_Theory.fact_space thy;
         val xname = Name_Space.extern_shortest thy_ctxt space name;
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
@@ -433,6 +467,25 @@
             export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)))
       else ();
 
+
+    (* other entities *)
+
+    fun export_other get_space =
+      let
+        val space = get_space thy;
+        val export_name = "other/" ^ Name_Space.kind_of space;
+        val decls = Name_Space.get_names space |> map (rpair ());
+      in export_entities export_name get_space decls (fn _ => fn () => SOME (K [])) end;
+
+    val other_spaces = other_name_spaces thy;
+    val other_kinds = map (fn get_space => Name_Space.kind_of (get_space thy)) other_spaces;
+    val _ =
+      if null other_kinds then ()
+      else
+        Export.export thy \<^path_binding>\<open>theory/other_kinds\<close>
+          (XML.Encode.string (cat_lines other_kinds));
+    val _ = List.app export_other other_spaces;
+
   in () end);
 
 end;

--- a/src/Pure/Thy/export_theory.scala	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Sep 07 21:16:22 2021 +0200
@@ -79,7 +79,8 @@
     constdefs: List[Constdef],
     typedefs: List[Typedef],
     datatypes: List[Datatype],
-    spec_rules: List[Spec_Rule])
+    spec_rules: List[Spec_Rule],
+    others: Map[String, List[Entity[Other]]])
   {
     override def toString: String = name
 
@@ -90,10 +91,11 @@
       thms.iterator.map(_.no_content) ++
       classes.iterator.map(_.no_content) ++
       locales.iterator.map(_.no_content) ++
-      locale_dependencies.iterator.map(_.no_content)
+      locale_dependencies.iterator.map(_.no_content) ++
+      (for { (_, xs) <- others; x <- xs.iterator } yield x.no_content)
 
-    lazy val entity_serials: Set[Long] =
-      entity_iterator.map(_.serial).toSet
+    lazy val entity_kinds: Set[String] =
+      entity_iterator.map(_.kind).toSet
 
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
@@ -110,7 +112,8 @@
         constdefs.map(_.cache(cache)),
         typedefs.map(_.cache(cache)),
         datatypes.map(_.cache(cache)),
-        spec_rules.map(_.cache(cache)))
+        spec_rules.map(_.cache(cache)),
+        (for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap)
   }
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
@@ -140,7 +143,8 @@
         read_constdefs(provider),
         read_typedefs(provider),
         read_datatypes(provider),
-        read_spec_rules(provider))
+        read_spec_rules(provider),
+        read_others(provider))
     if (cache.no_cache) theory else theory.cache(cache)
   }
 
@@ -168,21 +172,30 @@
 
   /* entities */
 
-  object Kind extends Enumeration
+  object Kind
   {
-    val TYPE = Value("type")
-    val CONST = Value("const")
-    val AXIOM = Value("axiom")
-    val THM = Value("thm")
-    val PROOF = Value("proof")
-    val CLASS = Value("class")
-    val LOCALE = Value("locale")
-    val LOCALE_DEPENDENCY = Value("locale_dependency")
-    val DOCUMENT_HEADING = Value("document_heading")
-    val DOCUMENT_TEXT = Value("document_text")
-    val PROOF_TEXT = Value("proof_text")
+    val TYPE = "type"
+    val CONST = "const"
+    val THM = "thm"
+    val PROOF = "proof"
+    val LOCALE_DEPENDENCY = "locale_dependency"
+    val DOCUMENT_HEADING = "document_heading"
+    val DOCUMENT_TEXT = "document_text"
+    val PROOF_TEXT = "proof_text"
+
+    def export(kind: String): String =
+      kind match {
+        case Markup.TYPE_NAME => TYPE
+        case Markup.CONSTANT => CONST
+        case _ => kind
+      }
   }
 
+  def export_kind(kind: String): String =
+    if (kind == Markup.TYPE_NAME) "type"
+    else if (kind == Markup.CONSTANT) "const"
+    else kind
+
   abstract class Content[T]
   {
     def cache(cache: Term.Cache): T
@@ -192,7 +205,7 @@
     def cache(cache: Term.Cache): No_Content = this
   }
   sealed case class Entity[A <: Content[A]](
-    kind: Kind.Value,
+    kind: String,
     name: String,
     xname: String,
     pos: Position.T,
@@ -200,7 +213,8 @@
     serial: Long,
     content: Option[A])
   {
-    override def toString: String = kind.toString + " " + quote(name)
+    def export_kind: String = Kind.export(kind)
+    override def toString: String = export_kind + " " + quote(name)
 
     def the_content: A =
       if (content.isDefined) content.get else error("No content for " + toString)
@@ -209,7 +223,7 @@
 
     def cache(cache: Term.Cache): Entity[A] =
       Entity(
-        kind,
+        cache.string(kind),
         cache.string(name),
         cache.string(xname),
         cache.position(pos),
@@ -221,7 +235,7 @@
   def read_entities[A <: Content[A]](
     provider: Export.Provider,
     export_name: String,
-    kind: Kind.Value,
+    kind: String,
     decode: XML.Decode.T[A]): List[Entity[A]] =
   {
     def decode_entity(tree: XML.Tree): Entity[A] =
@@ -279,7 +293,7 @@
   }
 
   def read_types(provider: Export.Provider): List[Entity[Type]] =
-    read_entities(provider, Export.THEORY_PREFIX + "types", Kind.TYPE, body =>
+    read_entities(provider, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME, body =>
       {
         import XML.Decode._
         val (syntax, args, abbrev) =
@@ -307,7 +321,7 @@
   }
 
   def read_consts(provider: Export.Provider): List[Entity[Const]] =
-    read_entities(provider, Export.THEORY_PREFIX + "consts", Kind.CONST, body =>
+    read_entities(provider, Export.THEORY_PREFIX + "consts", Markup.CONSTANT, body =>
       {
         import XML.Decode._
         val (syntax, (typargs, (typ, (abbrev, propositional)))) =
@@ -350,7 +364,7 @@
   }
 
   def read_axioms(provider: Export.Provider): List[Entity[Axiom]] =
-    read_entities(provider, Export.THEORY_PREFIX + "axioms", Kind.AXIOM,
+    read_entities(provider, Export.THEORY_PREFIX + "axioms", Markup.AXIOM,
       body => Axiom(decode_prop(body)))
 
 
@@ -476,7 +490,7 @@
   }
 
   def read_classes(provider: Export.Provider): List[Entity[Class]] =
-    read_entities(provider, Export.THEORY_PREFIX + "classes", Kind.CLASS, body =>
+    read_entities(provider, Export.THEORY_PREFIX + "classes", Markup.CLASS, body =>
       {
         import XML.Decode._
         import Term_XML.Decode._
@@ -500,7 +514,7 @@
   }
 
   def read_locales(provider: Export.Provider): List[Entity[Locale]] =
-    read_entities(provider, Export.THEORY_PREFIX + "locales", Kind.LOCALE, body =>
+    read_entities(provider, Export.THEORY_PREFIX + "locales", Markup.LOCALE, body =>
       {
         import XML.Decode._
         import Term_XML.Decode._
@@ -765,4 +779,26 @@
     for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
       yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)
   }
+
+
+  /* other entities */
+
+  sealed case class Other() extends Content[Other]
+  {
+    override def cache(cache: Term.Cache): Other = this
+  }
+
+  def read_others(provider: Export.Provider): Map[String, List[Entity[Other]]] =
+  {
+    val kinds =
+      provider(Export.THEORY_PREFIX + "other_kinds") match {
+        case Some(entry) => split_lines(entry.uncompressed.text)
+        case None => Nil
+      }
+    val other = Other()
+    def read_other(kind: String): List[Entity[Other]] =
+      read_entities(provider, Export.THEORY_PREFIX + "other/" + kind, kind, _ => other)
+
+    kinds.map(kind => kind -> read_other(kind)).toMap
+  }
 }

--- a/src/Pure/global_theory.ML	Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/global_theory.ML	Tue Sep 07 21:16:22 2021 +0200
@@ -7,6 +7,7 @@
 signature GLOBAL_THEORY =
 sig
   val facts_of: theory -> Facts.T
+  val fact_space: theory -> Name_Space.T
   val check_fact: theory -> xstring * Position.T -> string
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
@@ -73,6 +74,7 @@
 val facts_of = #1 o Data.get;
 val map_facts = Data.map o apfst;
 
+val fact_space = Facts.space_of o facts_of;
 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;