src/Pure/General/name_space.ML
changeset 50201 c26369c9eda6
parent 49816 e63d6c55ad6d
child 50301 56b4c9afd7be
equal deleted inserted replaced
50200:2c94c065564e 50201:c26369c9eda6
    86   theory_name: string,
    86   theory_name: string,
    87   pos: Position.T,
    87   pos: Position.T,
    88   id: serial};
    88   id: serial};
    89 
    89 
    90 fun entry_markup def kind (name, {pos, id, ...}: entry) =
    90 fun entry_markup def kind (name, {pos, id, ...}: entry) =
    91   Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
    91   Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
    92 
    92 
    93 fun print_entry_ref kind (name, entry) =
    93 fun print_entry_ref kind (name, entry) =
    94   quote (Markup.markup (entry_markup false kind (name, entry)) name);
    94   quote (Markup.markup (entry_markup false kind (name, entry)) name);
    95 
    95 
    96 fun err_dup kind entry1 entry2 pos =
    96 fun err_dup kind entry1 entry2 pos =
   131 
   131 
   132 fun entry_ord space = int_ord o pairself (#id o the_entry space);
   132 fun entry_ord space = int_ord o pairself (#id o the_entry space);
   133 
   133 
   134 fun markup (Name_Space {kind, entries, ...}) name =
   134 fun markup (Name_Space {kind, entries, ...}) name =
   135   (case Symtab.lookup entries name of
   135   (case Symtab.lookup entries name of
   136     NONE => Isabelle_Markup.intensify
   136     NONE => Markup.intensify
   137   | SOME (_, entry) => entry_markup false kind (name, entry));
   137   | SOME (_, entry) => entry_markup false kind (name, entry));
   138 
   138 
   139 fun is_concealed space name = #concealed (the_entry space name);
   139 fun is_concealed space name = #concealed (the_entry space name);
   140 
   140 
   141 
   141