--- 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;
--- 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;
--- 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;
--- 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;
--- 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 =
--- 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;
--- 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)]
--- 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)]
--- 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) =>
--- 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