more exports;
misc tuning and clarification;

--- 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;