--- a/src/Pure/General/name_space.ML Wed Apr 27 17:20:29 2011 +0200
+++ b/src/Pure/General/name_space.ML Wed Apr 27 17:44:06 2011 +0200
@@ -16,6 +16,7 @@
val kind_of: T -> string
val the_entry: T -> string ->
{concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
+ val entry_ord: T -> string * string -> order
val markup: T -> string -> Markup.T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
@@ -125,6 +126,8 @@
NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
| SOME (_, entry) => entry);
+fun entry_ord space = int_ord o pairself (#id o the_entry space);
+
fun markup (Name_Space {kind, entries, ...}) name =
(case Symtab.lookup entries name of
NONE => Markup.malformed