# HG changeset patch # User wenzelm # Date 1526219730 -7200 # Node ID a7a2174ac01491b29b8cad1802bdd9f7a382876f # Parent 738071699826eec2c743cb3ec7398f2c0bb0dbe1 more exports; misc tuning and clarification; diff -r 738071699826 -r a7a2174ac014 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun May 13 15:05:31 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun May 13 15:55:30 2018 +0200 @@ -6,56 +6,77 @@ signature EXPORT_THEORY = sig - val export_table_diff: ('a -> XML.tree list option) -> - 'a Name_Space.table list -> 'a Name_Space.table -> XML.tree list end; structure Export_Theory: EXPORT_THEORY = struct -(* export namespace table *) +(* name space entries *) -fun export_table_diff export_decl prev_tables table = - (table, []) |-> Name_Space.fold_table (fn (name, decl) => - if exists (fn prev => Name_Space.defined prev name) prev_tables then I +fun export_decls export_decl parents space decls = + (decls, []) |-> fold (fn (name, decl) => + if exists (fn space => Name_Space.declared space name) parents then I else (case export_decl decl of NONE => I | SOME body => - let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name + let val markup = Name_Space.markup_def space name in cons (name, XML.Elem (markup, body)) end)) |> sort_by #1 |> map #2; (* present *) -fun present get export name thy = +fun present get_space get_decls export name thy = if Options.default_bool "export_theory" then - (case export (map get (Theory.parents_of thy)) (get thy) of + (case export (map get_space (Theory.parents_of thy)) (get_space thy) (get_decls thy) of [] => () | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body]) else (); +fun present_decls get_space get_decls = + present get_space get_decls o export_decls; + +val setup_presentation = Theory.setup o Thy_Info.add_presentation; + (* types *) -val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff; +local -fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n) - | export_logical_type _ = NONE; +val present_types = + present_decls Sign.type_space (Name_Space.dest_table o #types o Type.rep_tsig o Sign.tsig_of); -fun export_abbreviation (Type.Abbreviation (vs, U, _)) = - let open XML.Encode Term_XML.Encode - in SOME (pair (list string) typ (vs, U)) end - | export_abbreviation _ = NONE; +val encode_type = + let open XML.Encode Term_XML.Encode + in pair (list string) (option typ) end; -fun export_nonterminal Type.Nonterminal = SOME [] - | export_nonterminal _ = NONE; +fun export_type (Type.LogicalType n) = SOME (encode_type (Name.invent Name.context Name.aT n, NONE)) + | export_type (Type.Abbreviation (args, U, false)) = SOME (encode_type (args, SOME U)) + | export_type _ = NONE; -val _ = - Theory.setup - (Thy_Info.add_presentation (present_types export_logical_type "types") #> - Thy_Info.add_presentation (present_types export_abbreviation "type_synonyms") #> - Thy_Info.add_presentation (present_types export_nonterminal "nonterminals")); +in + +val _ = setup_presentation (present_types export_type "types"); end; + + +(* consts *) + +local + +val present_consts = + present_decls Sign.const_space (#constants o Consts.dest o Sign.consts_of); + +val encode_const = + let open XML.Encode Term_XML.Encode + in pair typ (option term) end; + +in + +val _ = setup_presentation (present_consts (SOME o encode_const) "consts"); + +end; + +end;