# HG changeset patch
# User wenzelm
# Date 1526072340 -7200
# Node ID 42d63ea3916165c657c30b8b2f7a43b1b09d6e1c
# Parent  e469d529e6da7d85093bbbda6ad6b494ce1e54ae
some export of foundational theory content;

diff -r e469d529e6da -r 42d63ea39161 etc/options
--- a/etc/options	Fri May 11 22:40:02 2018 +0200
+++ b/etc/options	Fri May 11 22:59:00 2018 +0200
@@ -247,6 +247,11 @@
   -- "maximum number of messages to keep SSH server connection alive"
 
 
+section "Theory export"
+
+option export_theory : bool = false
+
+
 section "Build Log Database"
 
 option build_log_database_user : string = ""
diff -r e469d529e6da -r 42d63ea39161 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri May 11 22:40:02 2018 +0200
+++ b/src/Pure/ROOT.ML	Fri May 11 22:59:00 2018 +0200
@@ -303,6 +303,7 @@
 ML_file "Thy/export.ML";
 ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
+ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/protocol_message.ML";
diff -r e469d529e6da -r 42d63ea39161 src/Pure/Thy/export_theory.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/export_theory.ML	Fri May 11 22:59:00 2018 +0200
@@ -0,0 +1,61 @@
+(*  Title:      Pure/Thy/export_theory.ML
+    Author:     Makarius
+
+Export foundational theory content.
+*)
+
+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 *)
+
+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
+    else
+      (case export_decl decl of
+        NONE => I
+      | SOME body =>
+          let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name
+          in cons (name, XML.Elem (markup, body)) end))
+  |> sort_by #1 |> map #2;
+
+
+(* present *)
+
+fun present get export name thy =
+  if Options.default_bool "export_theory" then
+    (case export (map get (Theory.parents_of thy)) (get thy) of
+      [] => ()
+    | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
+  else ();
+
+
+(* types *)
+
+val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff;
+
+fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n)
+  | export_logical_type _ = NONE;
+
+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;
+
+fun export_nonterminal Type.Nonterminal = SOME []
+  | export_nonterminal _ = 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"));
+
+end;