# HG changeset patch
# User wenzelm
# Date 1628098919 -7200
# Node ID 700e5bd59c7dab47b99e8873023009394491b35a
# Parent  228adc5028038f32cf457607484b9eab86ae97a7
clarified export of formal entities: name space info is always present, but content depends on option "export_theory";

diff -r 228adc502803 -r 700e5bd59c7d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Aug 03 13:40:17 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Aug 04 19:41:59 2021 +0200
@@ -1240,31 +1240,34 @@
 
 (* theory export *)
 
-val _ = Export_Theory.setup_presentation (fn context => fn thy =>
-  let
-    val parents = map (Data.get o Context.Theory) (Theory.parents_of thy);
-    val datatypes =
-      (Data.get (Context.Theory thy), []) |-> Symtab.fold
-        (fn (name, (pos, {kind, T, ctrs, ...})) =>
-          if kind = Record orelse exists (fn tab => Symtab.defined tab name) parents then I
-          else
-            let
-              val pos_properties = Thy_Info.adjust_pos_properties context pos;
-              val typ = Logic.unvarifyT_global T;
-              val constrs = map Logic.unvarify_global ctrs;
-              val typargs = rev (fold Term.add_tfrees (Logic.mk_type typ :: constrs) []);
-              val constructors = map (fn t => (t, Term.type_of t)) constrs;
-            in
-              cons (pos_properties, (name, (kind = Codatatype, (typargs, (typ, constructors)))))
-            end);
-  in
-    if null datatypes then ()
-    else
-      Export_Theory.export_body thy "datatypes"
-        let open XML.Encode Term_XML.Encode in
-          list (pair properties (pair string (pair bool (pair (list (pair string sort))
-            (pair typ (list (pair (term (Sign.consts_of thy)) typ))))))) datatypes
-        end
-  end);
+val _ =
+  (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy =>
+    if Export_Theory.export_enabled context then
+      let
+        val parents = map (Data.get o Context.Theory) (Theory.parents_of thy);
+        val datatypes =
+          (Data.get (Context.Theory thy), []) |-> Symtab.fold
+            (fn (name, (pos, {kind, T, ctrs, ...})) =>
+              if kind = Record orelse exists (fn tab => Symtab.defined tab name) parents then I
+              else
+                let
+                  val pos_properties = Thy_Info.adjust_pos_properties context pos;
+                  val typ = Logic.unvarifyT_global T;
+                  val constrs = map Logic.unvarify_global ctrs;
+                  val typargs = rev (fold Term.add_tfrees (Logic.mk_type typ :: constrs) []);
+                  val constructors = map (fn t => (t, Term.type_of t)) constrs;
+                in
+                  cons (pos_properties, (name, (kind = Codatatype, (typargs, (typ, constructors)))))
+                end);
+      in
+        if null datatypes then ()
+        else
+          Export_Theory.export_body thy "datatypes"
+            let open XML.Encode Term_XML.Encode in
+              list (pair properties (pair string (pair bool (pair (list (pair string sort))
+                (pair typ (list (pair (term (Sign.consts_of thy)) typ))))))) datatypes
+            end
+      end
+    else ());
 
 end;
diff -r 228adc502803 -r 700e5bd59c7d src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Aug 03 13:40:17 2021 +0200
+++ b/src/HOL/Tools/typedef.ML	Wed Aug 04 19:41:59 2021 +0200
@@ -349,23 +349,26 @@
 
 (** theory export **)
 
-val _ = Export_Theory.setup_presentation (fn _ => fn thy =>
-  let
-    val parent_spaces = map Sign.type_space (Theory.parents_of thy);
-    val typedefs =
-      Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy)))
-      |> maps (fn (name, _) =>
-          if exists (fn space => Name_Space.declared space name) parent_spaces then []
-          else
-            get_info_global thy name
-            |> map (fn ({rep_type, abs_type, Rep_name, Abs_name, axiom_name}, _) =>
-              (name, (rep_type, (abs_type, (Rep_name, (Abs_name, axiom_name)))))));
-  in
-    if null typedefs then ()
-    else
-      Export_Theory.export_body thy "typedefs"
-        let open XML.Encode Term_XML.Encode
-        in list (pair string (pair typ (pair typ (pair string (pair string string))))) typedefs end
-  end);
+val _ =
+  (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy =>
+    if Export_Theory.export_enabled context then
+      let
+        val parent_spaces = map Sign.type_space (Theory.parents_of thy);
+        val typedefs =
+          Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy)))
+          |> maps (fn (name, _) =>
+              if exists (fn space => Name_Space.declared space name) parent_spaces then []
+              else
+                get_info_global thy name
+                |> map (fn ({rep_type, abs_type, Rep_name, Abs_name, axiom_name}, _) =>
+                  (name, (rep_type, (abs_type, (Rep_name, (Abs_name, axiom_name)))))));
+        val encode =
+          let open XML.Encode Term_XML.Encode
+          in list (pair string (pair typ (pair typ (pair string (pair string string))))) end;
+      in
+        if null typedefs then ()
+        else Export_Theory.export_body thy "typedefs" (encode typedefs)
+      end
+    else ());
 
 end;
diff -r 228adc502803 -r 700e5bd59c7d src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Aug 03 13:40:17 2021 +0200
+++ b/src/Pure/Thy/export_theory.ML	Wed Aug 04 19:41:59 2021 +0200
@@ -6,7 +6,7 @@
 
 signature EXPORT_THEORY =
 sig
-  val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
+  val export_enabled: Thy_Info.presentation_context -> bool
   val export_body: theory -> string -> XML.body -> unit
 end;
 
@@ -108,28 +108,33 @@
       in SOME (dep, (substT, subst)) end);
 
 
-(* general setup *)
+(* presentation *)
 
-fun setup_presentation f =
-  Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
-    if Options.bool (#options context) "export_theory" then f context thy else ()));
+fun export_enabled (context: Thy_Info.presentation_context) =
+  Options.bool (#options context) "export_theory";
 
 fun export_body thy name body =
   if XML.is_empty_body body then ()
   else Export.export thy (Path.binding0 (Path.make ["theory", name])) body;
 
-
-(* presentation *)
-
-val _ = setup_presentation (fn context => fn thy =>
+val _ = (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy =>
   let
-    val parents = Theory.parents_of thy;
     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
-
+    val consts = Sign.consts_of thy;
     val thy_ctxt = Proof_Context.init_global thy;
 
     val pos_properties = Thy_Info.adjust_pos_properties context;
 
+    val enabled = export_enabled context;
+
+
+    (* strict parents *)
+
+    val parents = Theory.parents_of thy;
+    val _ =
+      Export.export thy \<^path_binding>\<open>theory/parents\<close>
+        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
+
 
     (* spec rules *)
 
@@ -162,7 +167,7 @@
         val {serial, pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup name xname pos serial end;
 
-    fun export_entities export_name export get_space decls =
+    fun export_entities export_name get_space decls export =
       let
         val parent_spaces = map get_space parents;
         val space = get_space thy;
@@ -172,9 +177,11 @@
           else
             (case export name decl of
               NONE => I
-            | SOME body =>
-                cons (#serial (Name_Space.the_entry space name),
-                  XML.Elem (entity_markup space name, body))))
+            | SOME make_body =>
+                let
+                  val i = #serial (Name_Space.the_entry space name);
+                  val body = if enabled then make_body () else [];
+                in cons (i, XML.Elem (entity_markup space name, body)) end))
         |> sort (int_ord o apply2 #1) |> map #2
         |> export_body thy export_name
       end;
@@ -186,40 +193,40 @@
       let open XML.Encode Term_XML.Encode
       in triple encode_syntax (list string) (option typ) end;
 
-    fun export_type c (Type.LogicalType n) =
-          SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
-      | export_type c (Type.Abbreviation (args, U, false)) =
-          SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U))
-      | export_type _ _ = NONE;
-
     val _ =
-      export_entities "types" export_type Sign.type_space
-        (Name_Space.dest_table (#types rep_tsig));
+      export_entities "types" Sign.type_space (Name_Space.dest_table (#types rep_tsig))
+        (fn c =>
+          (fn Type.LogicalType n =>
+                SOME (fn () =>
+                  encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
+            | Type.Abbreviation (args, U, false) =>
+                SOME (fn () =>
+                  encode_type (get_syntax_type thy_ctxt c, args, SOME U))
+            | _ => NONE));
 
 
     (* consts *)
 
-    val consts = Sign.consts_of thy;
     val encode_term = Term_XML.Encode.term consts;
 
     val encode_const =
       let open XML.Encode Term_XML.Encode
       in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
 
-    fun export_const c (T, abbrev) =
-      let
-        val syntax = get_syntax_const thy_ctxt c;
-        val U = Logic.unvarifyT_global T;
-        val U0 = Type.strip_sorts U;
-        val abbrev' = abbrev
-          |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
-        val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
-        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
-      in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end;
-
     val _ =
-      export_entities "consts" (SOME oo export_const) Sign.const_space
-        (#constants (Consts.dest consts));
+      export_entities "consts" Sign.const_space (#constants (Consts.dest consts))
+        (fn c => fn (T, abbrev) =>
+          SOME (fn () =>
+            let
+              val syntax = get_syntax_const thy_ctxt c;
+              val U = Logic.unvarifyT_global T;
+              val U0 = Type.strip_sorts U;
+              val trim_abbrev =
+                Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts;
+              val abbrev' = Option.map trim_abbrev abbrev;
+              val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
+              val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
+            in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end));
 
 
     (* axioms *)
@@ -244,8 +251,8 @@
       encode_prop (#1 (standard_prop used [] prop NONE));
 
     val _ =
-      export_entities "axioms" (K (SOME o encode_axiom Name.context))
-        Theory.axiom_space (Theory.all_axioms_of thy);
+      export_entities "axioms" Theory.axiom_space (Theory.all_axioms_of thy)
+        (fn _ => fn prop => SOME (fn () => encode_axiom Name.context prop));
 
 
     (* theorems and proof terms *)
@@ -293,8 +300,12 @@
     fun export_thm (thm_id, thm_name) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
-        val thm = Global_Theory.get_thm_name thy (thm_name, Position.none);
-      in XML.Elem (markup, encode_thm thm_id thm) end;
+        val body =
+          if enabled then
+            Global_Theory.get_thm_name thy (thm_name, Position.none)
+            |> encode_thm thm_id
+          else [];
+      in XML.Elem (markup, body) end;
 
     val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy));
 
@@ -305,42 +316,44 @@
       let open XML.Encode Term_XML.Encode
       in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
 
-    fun export_class name =
-      (case try (Axclass.get_info thy) name of
-        NONE => ([], [])
-      | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
-      |> encode_class |> SOME;
-
     val _ =
-      export_entities "classes" (fn name => fn () => export_class name)
-        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
+      export_entities "classes" Sign.class_space
+        (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))))
+        (fn name => fn () => SOME (fn () =>
+          (case try (Axclass.get_info thy) name of
+            NONE => ([], [])
+          | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
+          |> encode_class));
 
 
     (* sort algebra *)
 
-    local
-      val prop = encode_axiom Name.context o Logic.varify_global;
+    val _ =
+      if enabled then
+        let
+          val prop = encode_axiom Name.context o Logic.varify_global;
 
-      val encode_classrel =
-        let open XML.Encode
-        in list (pair prop (pair string string)) end;
+          val encode_classrel =
+            let open XML.Encode
+            in list (pair prop (pair string string)) end;
+
+          val encode_arities =
+            let open XML.Encode Term_XML.Encode
+            in list (pair prop (triple string (list sort) string)) end;
 
-      val encode_arities =
-        let open XML.Encode Term_XML.Encode
-        in list (pair prop (triple string (list sort) string)) end;
-    in
-      val export_classrel =
-        maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
+          val export_classrel =
+            maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
+
+          val export_arities = map (`Logic.mk_arity) #> encode_arities;
 
-      val export_arities = map (`Logic.mk_arity) #> encode_arities;
-
-      val {classrel, arities} =
-        Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
-          (#2 (#classes rep_tsig));
-    end;
-
-    val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel);
-    val _ = if null arities then () else export_body thy "arities" (export_arities arities);
+          val {classrel, arities} =
+            Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
+              (#2 (#classes rep_tsig));
+        in
+          if null classrel then () else export_body thy "classrel" (export_classrel classrel);
+          if null arities then () else export_body thy "arities" (export_arities arities)
+        end
+      else ();
 
 
     (* locales *)
@@ -351,18 +364,16 @@
           (list (encode_axiom used))
       end;
 
-    fun export_locale loc =
-      let
-        val {typargs, args, axioms} = locale_content thy loc;
-        val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context;
-      in encode_locale used (typargs, args, axioms) end
-      handle ERROR msg =>
-        cat_error msg ("The error(s) above occurred in locale " ^
-          quote (Locale.markup_name thy_ctxt loc));
-
     val _ =
-      export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
-        Locale.locale_space (get_locales thy);
+      export_entities "locales" Locale.locale_space (get_locales thy)
+        (fn loc => fn () => SOME (fn () =>
+          let
+            val {typargs, args, axioms} = locale_content thy loc;
+            val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context;
+          in encode_locale used (typargs, args, axioms) end
+          handle ERROR msg =>
+            cat_error msg ("The error(s) above occurred in locale " ^
+              quote (Locale.markup_name thy_ctxt loc))));
 
 
     (* locale dependencies *)
@@ -376,29 +387,31 @@
         in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
 
     val _ =
-      get_dependencies parents thy
-      |> map_index (fn (i, dep) =>
-        let
-          val xname = string_of_int (i + 1);
-          val name = Long_Name.implode [Context.theory_name thy, xname];
-          val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
-          val body = encode_locale_dependency dep;
-        in XML.Elem (markup, body) end)
-      |> export_body thy "locale_dependencies";
+      if enabled then
+        get_dependencies parents thy |> map_index (fn (i, dep) =>
+          let
+            val xname = string_of_int (i + 1);
+            val name = Long_Name.implode [Context.theory_name thy, xname];
+            val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
+            val body = encode_locale_dependency dep;
+          in XML.Elem (markup, body) end)
+        |> export_body thy "locale_dependencies"
+      else ();
 
 
     (* constdefs *)
 
-    val constdefs =
-      Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy)
-      |> sort_by #1;
-
-    val encode_constdefs =
-      let open XML.Encode
-      in list (pair string string) end;
-
     val _ =
-      if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
+      if enabled then
+        let
+          val constdefs =
+            Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy)
+            |> sort_by #1;
+          val encode =
+            let open XML.Encode
+            in list (pair string string) end;
+        in if null constdefs then () else export_body thy "constdefs" (encode constdefs) end
+      else ();
 
 
     (* spec rules *)
@@ -413,16 +426,12 @@
       end;
 
     val _ =
-      (case Spec_Rules.dest_theory thy of
-        [] => ()
-      | spec_rules => export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)));
-
-
-    (* parents *)
-
-    val _ =
-      Export.export thy \<^path_binding>\<open>theory/parents\<close>
-        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
+      if enabled then
+        (case Spec_Rules.dest_theory thy of
+          [] => ()
+        | spec_rules =>
+            export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)))
+      else ();
 
   in () end);
 
diff -r 228adc502803 -r 700e5bd59c7d src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 03 13:40:17 2021 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Aug 04 19:41:59 2021 +0200
@@ -67,13 +67,13 @@
   /** theory content **/
 
   sealed case class Theory(name: String, parents: List[String],
-    types: List[Type],
-    consts: List[Const],
-    axioms: List[Axiom],
-    thms: List[Thm],
-    classes: List[Class],
-    locales: List[Locale],
-    locale_dependencies: List[Locale_Dependency],
+    types: List[Entity[Type]],
+    consts: List[Entity[Const]],
+    axioms: List[Entity[Axiom]],
+    thms: List[Entity[Thm]],
+    classes: List[Entity[Class]],
+    locales: List[Entity[Locale]],
+    locale_dependencies: List[Entity[Locale_Dependency]],
     classrel: List[Classrel],
     arities: List[Arity],
     constdefs: List[Constdef],
@@ -83,14 +83,14 @@
   {
     override def toString: String = name
 
-    def entity_iterator: Iterator[Entity] =
-      types.iterator.map(_.entity) ++
-      consts.iterator.map(_.entity) ++
-      axioms.iterator.map(_.entity) ++
-      thms.iterator.map(_.entity) ++
-      classes.iterator.map(_.entity) ++
-      locales.iterator.map(_.entity) ++
-      locale_dependencies.iterator.map(_.entity)
+    def entity_iterator: Iterator[Entity[No_Content]] =
+      types.iterator.map(_.no_content) ++
+      consts.iterator.map(_.no_content) ++
+      axioms.iterator.map(_.no_content) ++
+      thms.iterator.map(_.no_content) ++
+      classes.iterator.map(_.no_content) ++
+      locales.iterator.map(_.no_content) ++
+      locale_dependencies.iterator.map(_.no_content)
 
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
@@ -180,29 +180,64 @@
     val PROOF_TEXT = Value("proof_text")
   }
 
-  sealed case class Entity(
-    kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
+  abstract class Content[T]
+  {
+    def cache(cache: Term.Cache): T
+  }
+  sealed case class No_Content() extends Content[No_Content]
+  {
+    def cache(cache: Term.Cache): No_Content = this
+  }
+  sealed case class Entity[A <: Content[A]](
+    kind: Kind.Value,
+    name: String,
+    xname: String,
+    pos: Position.T,
+    id: Option[Long],
+    serial: Long,
+    content: Option[A])
   {
     override def toString: String = kind.toString + " " + quote(name)
 
-    def cache(cache: Term.Cache): Entity =
-      Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
+    def the_content: A =
+      if (content.isDefined) content.get else error("No content for " + toString)
+
+    def no_content: Entity[No_Content] = copy(content = None)
+
+    def cache(cache: Term.Cache): Entity[A] =
+      Entity(
+        kind,
+        cache.string(name),
+        cache.string(xname),
+        cache.position(pos),
+        id,
+        serial,
+        content.map(_.cache(cache)))
   }
 
-  def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
+  def read_entities[A <: Content[A]](
+    provider: Export.Provider,
+    export_name: String,
+    kind: Kind.Value,
+    decode: XML.Decode.T[A]): List[Entity[A]] =
   {
-    def err(): Nothing = throw new XML.XML_Body(List(tree))
+    def decode_entity(tree: XML.Tree): Entity[A] =
+    {
+      def err(): Nothing = throw new XML.XML_Body(List(tree))
 
-    tree match {
-      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
-        val name = Markup.Name.unapply(props) getOrElse err()
-        val xname = Markup.XName.unapply(props) getOrElse err()
-        val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
-        val id = Position.Id.unapply(props)
-        val serial = Markup.Serial.unapply(props) getOrElse err()
-        (Entity(kind, name, xname, pos, id, serial), body)
-      case _ => err()
+      tree match {
+        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
+          val name = Markup.Name.unapply(props) getOrElse err()
+          val xname = Markup.XName.unapply(props) getOrElse err()
+          val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
+          val id = Position.Id.unapply(props)
+          val serial = Markup.Serial.unapply(props) getOrElse err()
+          val content = if (body.isEmpty) None else Some(decode(body))
+          Entity(kind, name, xname, pos, id, serial, content)
+        case _ => err()
+      }
     }
+    provider.uncompressed_yxml(export_name).map(decode_entity)
   }
 
 
@@ -230,41 +265,37 @@
 
   /* types */
 
-  sealed case class Type(
-    entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
+  sealed case class Type(syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
+    extends Content[Type]
   {
-    def cache(cache: Term.Cache): Type =
-      Type(entity.cache(cache),
+    override def cache(cache: Term.Cache): Type =
+      Type(
         syntax,
         args.map(cache.string),
         abbrev.map(cache.typ))
   }
 
-  def read_types(provider: Export.Provider): List[Type] =
-    provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) =>
+  def read_types(provider: Export.Provider): List[Entity[Type]] =
+    read_entities(provider, Export.THEORY_PREFIX + "types", Kind.TYPE, body =>
       {
-        val (entity, body) = decode_entity(Kind.TYPE, tree)
+        import XML.Decode._
         val (syntax, args, abbrev) =
-        {
-          import XML.Decode._
           triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
-        }
-        Type(entity, syntax, args, abbrev)
+        Type(syntax, args, abbrev)
       })
 
 
   /* consts */
 
   sealed case class Const(
-    entity: Entity,
     syntax: Syntax,
     typargs: List[String],
     typ: Term.Typ,
     abbrev: Option[Term.Term],
-    propositional: Boolean)
+    propositional: Boolean) extends Content[Const]
   {
-    def cache(cache: Term.Cache): Const =
-      Const(entity.cache(cache),
+    override def cache(cache: Term.Cache): Const =
+      Const(
         syntax,
         typargs.map(cache.string),
         cache.typ(typ),
@@ -272,19 +303,16 @@
         propositional)
   }
 
-  def read_consts(provider: Export.Provider): List[Const] =
-    provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) =>
+  def read_consts(provider: Export.Provider): List[Entity[Const]] =
+    read_entities(provider, Export.THEORY_PREFIX + "consts", Kind.CONST, body =>
       {
-        val (entity, body) = decode_entity(Kind.CONST, tree)
+        import XML.Decode._
         val (syntax, (typargs, (typ, (abbrev, propositional)))) =
-        {
-          import XML.Decode._
           pair(decode_syntax,
             pair(list(string),
               pair(Term_XML.Decode.typ,
                 pair(option(Term_XML.Decode.term), bool))))(body)
-        }
-        Const(entity, syntax, typargs, typ, abbrev, propositional)
+        Const(syntax, typargs, typ, abbrev, propositional)
       })
 
 
@@ -293,9 +321,9 @@
   sealed case class Prop(
     typargs: List[(String, Term.Sort)],
     args: List[(String, Term.Typ)],
-    term: Term.Term)
+    term: Term.Term) extends Content[Prop]
   {
-    def cache(cache: Term.Cache): Prop =
+    override def cache(cache: Term.Cache): Prop =
       Prop(
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
@@ -313,19 +341,14 @@
     Prop(typargs, args, t)
   }
 
-  sealed case class Axiom(entity: Entity, prop: Prop)
+  sealed case class Axiom(prop: Prop) extends Content[Axiom]
   {
-    def cache(cache: Term.Cache): Axiom =
-      Axiom(entity.cache(cache), prop.cache(cache))
+    override def cache(cache: Term.Cache): Axiom = Axiom(prop.cache(cache))
   }
 
-  def read_axioms(provider: Export.Provider): List[Axiom] =
-    provider.uncompressed_yxml(Export.THEORY_PREFIX + "axioms").map((tree: XML.Tree) =>
-      {
-        val (entity, body) = decode_entity(Kind.AXIOM, tree)
-        val prop = decode_prop(body)
-        Axiom(entity, prop)
-      })
+  def read_axioms(provider: Export.Provider): List[Entity[Axiom]] =
+    read_entities(provider, Export.THEORY_PREFIX + "axioms", Kind.AXIOM,
+      body => Axiom(decode_prop(body)))
 
 
   /* theorems */
@@ -336,30 +359,24 @@
   }
 
   sealed case class Thm(
-    entity: Entity,
     prop: Prop,
     deps: List[String],
-    proof: Term.Proof)
+    proof: Term.Proof) extends Content[Thm]
   {
-    def cache(cache: Term.Cache): Thm =
+    override def cache(cache: Term.Cache): Thm =
       Thm(
-        entity.cache(cache),
         prop.cache(cache),
         deps.map(cache.string),
         cache.proof(proof))
   }
 
-  def read_thms(provider: Export.Provider): List[Thm] =
-    provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) =>
+  def read_thms(provider: Export.Provider): List[Entity[Thm]] =
+    read_entities(provider, Export.THEORY_PREFIX + "thms", Kind.THM, body =>
       {
-        val (entity, body) = decode_entity(Kind.THM, tree)
-        val (prop, deps, prf) =
-        {
-          import XML.Decode._
-          import Term_XML.Decode._
-          triple(decode_prop, list(string), proof)(body)
-        }
-        Thm(entity, prop, deps, prf)
+        import XML.Decode._
+        import Term_XML.Decode._
+        val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body)
+        Thm(prop, deps, prf)
       })
 
   sealed case class Proof(
@@ -446,71 +463,62 @@
 
   /* type classes */
 
-  sealed case class Class(
-    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop])
+  sealed case class Class(params: List[(String, Term.Typ)], axioms: List[Prop])
+    extends Content[Class]
   {
-    def cache(cache: Term.Cache): Class =
-      Class(entity.cache(cache),
+    override def cache(cache: Term.Cache): Class =
+      Class(
         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         axioms.map(_.cache(cache)))
   }
 
-  def read_classes(provider: Export.Provider): List[Class] =
-    provider.uncompressed_yxml(Export.THEORY_PREFIX + "classes").map((tree: XML.Tree) =>
+  def read_classes(provider: Export.Provider): List[Entity[Class]] =
+    read_entities(provider, Export.THEORY_PREFIX + "classes", Kind.CLASS, body =>
       {
-        val (entity, body) = decode_entity(Kind.CLASS, tree)
-        val (params, axioms) =
-        {
-          import XML.Decode._
-          import Term_XML.Decode._
-          pair(list(pair(string, typ)), list(decode_prop))(body)
-        }
-        Class(entity, params, axioms)
+        import XML.Decode._
+        import Term_XML.Decode._
+        val (params, axioms) = pair(list(pair(string, typ)), list(decode_prop))(body)
+        Class(params, axioms)
       })
 
 
   /* locales */
 
   sealed case class Locale(
-    entity: Entity,
     typargs: List[(String, Term.Sort)],
     args: List[((String, Term.Typ), Syntax)],
-    axioms: List[Prop])
+    axioms: List[Prop]) extends Content[Locale]
   {
-    def cache(cache: Term.Cache): Locale =
-      Locale(entity.cache(cache),
+    override def cache(cache: Term.Cache): Locale =
+      Locale(
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
         axioms.map(_.cache(cache)))
   }
 
-  def read_locales(provider: Export.Provider): List[Locale] =
-    provider.uncompressed_yxml(Export.THEORY_PREFIX + "locales").map((tree: XML.Tree) =>
+  def read_locales(provider: Export.Provider): List[Entity[Locale]] =
+    read_entities(provider, Export.THEORY_PREFIX + "locales", Kind.LOCALE, body =>
       {
-        val (entity, body) = decode_entity(Kind.LOCALE, tree)
+        import XML.Decode._
+        import Term_XML.Decode._
         val (typargs, args, axioms) =
-        {
-          import XML.Decode._
-          import Term_XML.Decode._
           triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
             list(decode_prop))(body)
-        }
-        Locale(entity, typargs, args, axioms)
+        Locale(typargs, args, axioms)
       })
 
 
   /* locale dependencies */
 
   sealed case class Locale_Dependency(
-    entity: Entity,
     source: String,
     target: String,
     prefix: List[(String, Boolean)],
     subst_types: List[((String, Term.Sort), Term.Typ)],
-    subst_terms: List[((String, Term.Typ), Term.Term)])
+    subst_terms: List[((String, Term.Typ), Term.Term)]) extends Content[Locale_Dependency]
   {
-    def cache(cache: Term.Cache): Locale_Dependency =
-      Locale_Dependency(entity.cache(cache),
+    override def cache(cache: Term.Cache): Locale_Dependency =
+      Locale_Dependency(
         cache.string(source),
         cache.string(target),
         prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
@@ -521,19 +529,17 @@
       subst_types.isEmpty && subst_terms.isEmpty
   }
 
-  def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
-    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)))) =
+  def read_locale_dependencies(provider: Export.Provider): List[Entity[Locale_Dependency]] =
+    read_entities(provider, Export.THEORY_PREFIX + "locale_dependencies", Kind.LOCALE_DEPENDENCY,
+      body =>
         {
           import XML.Decode._
           import Term_XML.Decode._
-          pair(string, pair(string, pair(list(pair(string, bool)),
-            pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
-        }
-        Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms)
-      })
+          val (source, (target, (prefix, (subst_types, subst_terms)))) =
+            pair(string, pair(string, pair(list(pair(string, bool)),
+              pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
+          Locale_Dependency(source, target, prefix, subst_types, subst_terms)
+        })
 
 
   /* sort algebra */