src/Pure/General/name_space.ML
changeset 42487 398d7d6bba42
parent 42466 bbce02fcba60
child 42493 01430341fc79
equal deleted inserted replaced
42486:01b03a124b81 42487:398d7d6bba42
    14   type T
    14   type T
    15   val empty: string -> T
    15   val empty: string -> T
    16   val kind_of: T -> string
    16   val kind_of: T -> string
    17   val the_entry: T -> string ->
    17   val the_entry: T -> string ->
    18     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
    18     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
       
    19   val entry_ord: T -> string * string -> order
    19   val markup: T -> string -> Markup.T
    20   val markup: T -> string -> Markup.T
    20   val is_concealed: T -> string -> bool
    21   val is_concealed: T -> string -> bool
    21   val intern: T -> xstring -> string
    22   val intern: T -> xstring -> string
    22   val long_names_default: bool Unsynchronized.ref
    23   val long_names_default: bool Unsynchronized.ref
    23   val long_names_raw: Config.raw
    24   val long_names_raw: Config.raw
   123 fun the_entry (Name_Space {kind, entries, ...}) name =
   124 fun the_entry (Name_Space {kind, entries, ...}) name =
   124   (case Symtab.lookup entries name of
   125   (case Symtab.lookup entries name of
   125     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   126     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   126   | SOME (_, entry) => entry);
   127   | SOME (_, entry) => entry);
   127 
   128 
       
   129 fun entry_ord space = int_ord o pairself (#id o the_entry space);
       
   130 
   128 fun markup (Name_Space {kind, entries, ...}) name =
   131 fun markup (Name_Space {kind, entries, ...}) name =
   129   (case Symtab.lookup entries name of
   132   (case Symtab.lookup entries name of
   130     NONE => Markup.malformed
   133     NONE => Markup.malformed
   131   | SOME (_, entry) => entry_markup false kind (name, entry));
   134   | SOME (_, entry) => entry_markup false kind (name, entry));
   132 
   135