src/Pure/General/name_space.ML
changeset 59883 12a89103cae6
parent 59881 547bf78e5d4d
child 59884 bbf49d7dfd6f
equal deleted inserted replaced
59882:ada832308efe 59883:12a89103cae6
    10 signature NAME_SPACE =
    10 signature NAME_SPACE =
    11 sig
    11 sig
    12   type T
    12   type T
    13   val empty: string -> T
    13   val empty: string -> T
    14   val kind_of: T -> string
    14   val kind_of: T -> string
    15   val defined_entry: T -> string -> bool
       
    16   val the_entry: T -> string ->
    15   val the_entry: T -> string ->
    17     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
    16     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
    18   val entry_ord: T -> string * string -> order
    17   val entry_ord: T -> string * string -> order
    19   val markup: T -> string -> Markup.T
    18   val markup: T -> string -> Markup.T
    20   val is_concealed: T -> string -> bool
    19   val is_concealed: T -> string -> bool
    60   val change_ignore: 'a table -> 'a table
    59   val change_ignore: 'a table -> 'a table
    61   val space_of_table: 'a table -> T
    60   val space_of_table: 'a table -> T
    62   val check_reports: Context.generic -> 'a table ->
    61   val check_reports: Context.generic -> 'a table ->
    63     xstring * Position.T list -> (string * Position.report list) * 'a
    62     xstring * Position.T list -> (string * Position.report list) * 'a
    64   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    63   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
       
    64   val defined: 'a table -> string -> bool
    65   val lookup_key: 'a table -> string -> (string * 'a) option
    65   val lookup_key: 'a table -> string -> (string * 'a) option
    66   val get: 'a table -> string -> 'a
    66   val get: 'a table -> string -> 'a
    67   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    67   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    68   val alias_table: naming -> binding -> string -> 'a table -> 'a table
    68   val alias_table: naming -> binding -> string -> 'a table -> 'a table
    69   val hide_table: bool -> string -> 'a table -> 'a table
    69   val hide_table: bool -> string -> 'a table -> 'a table
   144 
   144 
   145 
   145 
   146 fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
   146 fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
   147 
   147 
   148 fun kind_of (Name_Space {kind, ...}) = kind;
   148 fun kind_of (Name_Space {kind, ...}) = kind;
   149 
       
   150 fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
       
   151 
   149 
   152 fun the_entry (Name_Space {kind, entries, ...}) name =
   150 fun the_entry (Name_Space {kind, entries, ...}) name =
   153   (case Change_Table.lookup entries name of
   151   (case Change_Table.lookup entries name of
   154     NONE => error (undefined kind name)
   152     NONE => error (undefined kind name)
   155   | SOME (_, entry) => entry);
   153   | SOME (_, entry) => entry);
   495   let
   493   let
   496     val ((name, reports), x) = check_reports context table (xname, [pos]);
   494     val ((name, reports), x) = check_reports context table (xname, [pos]);
   497     val _ = Position.reports reports;
   495     val _ = Position.reports reports;
   498   in (name, x) end;
   496   in (name, x) end;
   499 
   497 
       
   498 fun defined (Table (_, tab)) name = Change_Table.defined tab name;
   500 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
   499 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
   501 
   500 
   502 fun get table name =
   501 fun get table name =
   503   (case lookup_key table name of
   502   (case lookup_key table name of
   504     SOME (_, x) => x
   503     SOME (_, x) => x