# HG changeset patch
# User wenzelm
# Date 1394544519 -3600
# Node ID 4873054cd1fca6ff02add2015ffac7e591227788
# Parent  c3681b9e060f0354c86c4f931ffbb8b54fe5d70f
tuned signature;

diff -r c3681b9e060f -r 4873054cd1fc src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -230,7 +230,7 @@
     [Pretty.block
       (Pretty.breaks
         (Pretty.str "(co)inductives:" ::
-          map (Pretty.mark_str o #1) (Name_Space.extern_table' ctxt space infos))),
+          map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
   end |> Pretty.chunks |> Pretty.writeln;
 
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -71,10 +71,10 @@
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
     'a table * 'a table -> 'a table
-  val dest_table': Proof.context -> T -> 'a Symtab.table -> ((string * xstring) * 'a) list
-  val dest_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
-  val extern_table': Proof.context -> T -> 'a Symtab.table -> ((Markup.T * xstring) * 'a) list
-  val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
+  val extern_entries: Proof.context -> T -> (string * 'a) list -> ((string * xstring) * 'a) list
+  val markup_entries: Proof.context -> T -> (string * 'a) list -> ((Markup.T * xstring) * 'a) list
+  val extern_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
+  val markup_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
 end;
 
 structure Name_Space: NAME_SPACE =
@@ -536,17 +536,16 @@
 
 (* present table content *)
 
-fun dest_table' ctxt space tab =
-  Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
+fun extern_entries ctxt space entries =
+  fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries []
   |> Library.sort_wrt (#2 o #1);
 
-fun dest_table ctxt (Table (space, tab)) = dest_table' ctxt space tab;
-
-fun extern_table' ctxt space tab =
-  dest_table' ctxt space tab
+fun markup_entries ctxt space entries =
+  extern_entries ctxt space entries
   |> map (fn ((name, xname), x) => ((markup space name, xname), x));
 
-fun extern_table ctxt (Table (space, tab)) = extern_table' ctxt space tab;
+fun extern_table ctxt (Table (space, tab)) = extern_entries ctxt space (Symtab.dest tab);
+fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Symtab.dest tab);
 
 end;
 
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -104,7 +104,7 @@
           Pretty.block
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
-    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
+    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
@@ -337,7 +337,9 @@
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
     val space = attribute_space ctxt;
-    val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
+    val configs =
+      Name_Space.markup_entries ctxt space
+        (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt)));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
 
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Isar/bundle.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -133,7 +133,7 @@
       Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
         Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
   in
-    map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
+    map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
   end |> Pretty.chunks |> Pretty.writeln;
 
 end;
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -635,7 +635,7 @@
     (Pretty.breaks
       (Pretty.str "locales:" ::
         map (Pretty.mark_str o #1)
-          (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy))))
+          (Name_Space.markup_table (Proof_Context.init_global thy) (Locales.get thy))))
   |> Pretty.writeln;
 
 fun pretty_locale thy show_facts name =
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Isar/method.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -328,7 +328,7 @@
           Pretty.block
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
-    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
+    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -1236,7 +1236,7 @@
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
     val abbrevs =
-      Name_Space.extern_table' ctxt space (Symtab.make (Symtab.fold add_abbr constants []));
+      Name_Space.markup_entries ctxt space (Symtab.fold add_abbr constants []);
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -104,8 +104,8 @@
 fun print_antiquotations ctxt =
   let
     val (commands, options) = get_antiquotations ctxt;
-    val command_names = map #1 (Name_Space.extern_table ctxt commands);
-    val option_names = map #1 (Name_Space.extern_table ctxt options);
+    val command_names = map #1 (Name_Space.markup_table ctxt commands);
+    val option_names = map #1 (Name_Space.markup_table ctxt options);
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
       Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/display.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -157,22 +157,24 @@
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
-      Name_Space.dest_table' ctxt class_space
-        (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)))
+      Name_Space.extern_entries ctxt class_space
+        (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
       |> map (apfst #1);
-    val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1);
-    val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1);
+    val tdecls = Name_Space.extern_table ctxt types |> map (apfst #1);
+    val arties =
+      Name_Space.extern_entries ctxt (Type.type_space tsig) (Symtab.dest arities)
+      |> map (apfst #1);
 
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
     val cnsts =
-      Name_Space.extern_table' ctxt const_space
-        (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants)));
+      Name_Space.markup_entries ctxt const_space
+        (filter_out (prune_const o fst) (Symtab.dest constants));
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = Name_Space.extern_table' ctxt const_space constraints;
+    val cnstrs = Name_Space.markup_entries ctxt const_space (Symtab.dest constraints);
 
-    val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy);
+    val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
diff -r c3681b9e060f -r 4873054cd1fc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/thm.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -1743,7 +1743,7 @@
 );
 
 fun extern_oracles ctxt =
-  map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
+  map #1 (Name_Space.markup_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
 
 fun add_oracle (b, oracle) thy =
   let