--- a/src/HOL/Real_Asymp/exp_log_expression.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Wed Aug 04 21:00:37 2021 +0200
@@ -128,7 +128,7 @@
fun eq_entry ({name = name1, ...}, {name = name2, ...}) = (name1 = name2)
val empty =
{
- name_table = Name_Space.empty_table "Exp-Log Custom Function",
+ name_table = Name_Space.empty_table "exp_log_custom_function",
net = Item_Net.init eq_entry (fn {net_pat, ...} => [net_pat])
}
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Wed Aug 04 21:00:37 2021 +0200
@@ -135,7 +135,7 @@
structure Data = Generic_Data
(
type T = (Proof.context -> int -> tactic) Name_Space.table;
- val empty : T = Name_Space.empty_table "sign oracle tactics";
+ val empty : T = Name_Space.empty_table "sign_oracle_tactic";
val extend = I;
fun merge (tactics1, tactics2) : T = Name_Space.merge_tables (tactics1, tactics2);
);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Aug 04 21:00:37 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;
--- a/src/HOL/Tools/typedef.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/HOL/Tools/typedef.ML Wed Aug 04 21:00:37 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;
--- a/src/Pure/Isar/attrib.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 04 21:00:37 2021 +0200
@@ -93,7 +93,7 @@
structure Attributes = Generic_Data
(
type T = ((Token.src -> attribute) * string) Name_Space.table;
- val empty : T = Name_Space.empty_table "attribute";
+ val empty : T = Name_Space.empty_table Markup.attributeN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
--- a/src/Pure/Isar/locale.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/Isar/locale.ML Wed Aug 04 21:00:37 2021 +0200
@@ -177,7 +177,7 @@
structure Locales = Theory_Data
(
type T = locale Name_Space.table;
- val empty : T = Name_Space.empty_table "locale";
+ val empty : T = Name_Space.empty_table Markup.localeN;
val extend = I;
val merge = Name_Space.join_tables (K merge_locale);
);
--- a/src/Pure/Isar/method.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/Isar/method.ML Wed Aug 04 21:00:37 2021 +0200
@@ -292,7 +292,7 @@
ml_tactic: (morphism -> thm list -> tactic) option,
facts: thm list option};
val empty : T =
- {methods = Name_Space.empty_table "method", ml_tactic = NONE, facts = NONE};
+ {methods = Name_Space.empty_table Markup.methodN, ml_tactic = NONE, facts = NONE};
val extend = I;
fun merge
({methods = methods1, ml_tactic = ml_tactic1, facts = facts1},
--- a/src/Pure/PIDE/markup.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Aug 04 21:00:37 2021 +0200
@@ -89,12 +89,18 @@
val sessionN: string
val theoryN: string
val classN: string
+ val localeN: string
val type_nameN: string
val constantN: string
+ val axiomN: string
+ val factN: string
+ val oracleN: string
val fixedN: string val fixed: string -> T
val caseN: string val case_: string -> T
val dynamic_factN: string val dynamic_fact: string -> T
val literal_factN: string val literal_fact: string -> T
+ val attributeN: string
+ val methodN: string
val method_modifierN: string
val tfreeN: string val tfree: T
val tvarN: string val tvar: T
@@ -461,14 +467,20 @@
val theoryN = "theory";
val classN = "class";
+val localeN = "locale";
val type_nameN = "type_name";
val constantN = "constant";
+val axiomN = "axiom";
+val factN = "fact";
+val oracleN = "oracle";
val (fixedN, fixed) = markup_string "fixed" nameN;
val (caseN, case_) = markup_string "case" nameN;
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
+val attributeN = "attribute";
+val methodN = "method";
val method_modifierN = "method_modifier";
--- a/src/Pure/PIDE/markup.scala Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Aug 04 21:00:37 2021 +0200
@@ -292,13 +292,25 @@
/* misc entities */
+ val SESSION = "session"
+
val THEORY = "theory"
val CLASS = "class"
+ val LOCALE = "locale"
val TYPE_NAME = "type_name"
+ val CONSTANT = "constant"
+ val AXIOM = "axiom"
+ val FACT = "fact"
+ val ORACLE = "oracle"
+
val FIXED = "fixed"
val CASE = "case"
- val CONSTANT = "constant"
val DYNAMIC_FACT = "dynamic_fact"
+ val LITERAL_FACT = "literal_fact"
+
+ val ATTRIBUTE = "attribute"
+ val METHOD = "method"
+ val METHOD_MODIFIER = "method_modifier"
/* inner syntax */
@@ -321,9 +333,6 @@
val TYPING = "typing"
val CLASS_PARAMETER = "class_parameter"
- val ATTRIBUTE = "attribute"
- val METHOD = "method"
-
/* antiquotations */
--- a/src/Pure/Thy/export_theory.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/Thy/export_theory.ML Wed Aug 04 21:00:37 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);
--- a/src/Pure/Thy/export_theory.scala Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/Thy/export_theory.scala Wed Aug 04 21:00:37 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 */
--- a/src/Pure/facts.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/facts.ML Wed Aug 04 21:00:37 2021 +0200
@@ -146,7 +146,7 @@
fun make_facts facts props = Facts {facts = facts, props = props};
-val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
+val empty = make_facts (Name_Space.empty_table Markup.factN) Net.empty;
(* named facts *)
--- a/src/Pure/theory.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/theory.ML Wed Aug 04 21:00:37 2021 +0200
@@ -88,7 +88,7 @@
(
type T = thy;
val extend = I;
- val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], []));
+ val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
fun merge old_thys (thy1, thy2) =
let
val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
--- a/src/Pure/thm.ML Wed Aug 04 08:27:16 2021 +0200
+++ b/src/Pure/thm.ML Wed Aug 04 21:00:37 2021 +0200
@@ -897,7 +897,7 @@
unit Name_Space.table * (*oracles: authentic derivation names*)
classes; (*type classes within the logic*)
- val empty : T = (Name_Space.empty_table "oracle", empty_classes);
+ val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes);
val extend = I;
fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
(Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2));