# HG changeset patch
# User wenzelm
# Date 930598730 -7200
# Node ID 598d2f32d452945e1f7f8b9dab81a306f6f40aed
# Parent  3909657a7da69f7f33fa379c2c03d00b38c971b9
added cond_extern_table;

diff -r 3909657a7da6 -r 598d2f32d452 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Jun 25 13:37:51 1999 +0200
+++ b/src/Pure/General/name_space.ML	Mon Jun 28 21:38:50 1999 +0200
@@ -26,6 +26,7 @@
   val extern: T -> string -> string
   val long_names: bool ref
   val cond_extern: T -> string -> string
+  val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
   val dest: T -> (string * string list) list
 end;
 
@@ -103,6 +104,9 @@
 
 fun cond_extern space = if ! long_names then I else extern space;
 
+fun cond_extern_table space tab =
+  Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
+
 
 (* dest *)
 
diff -r 3909657a7da6 -r 598d2f32d452 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jun 25 13:37:51 1999 +0200
+++ b/src/Pure/sign.ML	Mon Jun 28 21:38:50 1999 +0200
@@ -55,6 +55,7 @@
   val intern: sg -> string -> xstring -> string
   val extern: sg -> string -> string -> xstring
   val cond_extern: sg -> string -> string -> xstring
+  val cond_extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
   val intern_class: sg -> xclass -> class
   val intern_tycon: sg -> xstring -> string
   val intern_const: sg -> xstring -> string
@@ -410,6 +411,7 @@
 fun intrn spaces kind = NameSpace.intern (space_of spaces kind);
 fun extrn spaces kind = NameSpace.extern (space_of spaces kind);
 fun cond_extrn spaces kind = NameSpace.cond_extern (space_of spaces kind);
+fun cond_extrn_table spaces kind tab = NameSpace.cond_extern_table (space_of spaces kind) tab;
 
 (*add names*)
 fun add_names spaces kind names =
@@ -471,6 +473,7 @@
   val intern = intrn o spaces_of;
   val extern = extrn o spaces_of;
   val cond_extern = cond_extrn o spaces_of;
+  fun cond_extern_table sg = cond_extrn_table (spaces_of sg);
 
   val intern_class = intrn_class o spaces_of;
   val intern_sort = intrn_sort o spaces_of;