src/Pure/General/table.ML
changeset 31209 77da3aad5917
parent 30647 ef8f46c3158a
child 31616 63893e3a50a6
equal deleted inserted replaced
31208:1ef2f0af7f26 31209:77da3aad5917
    31   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
    31   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
    32   val min_key: 'a table -> key option
    32   val min_key: 'a table -> key option
    33   val max_key: 'a table -> key option
    33   val max_key: 'a table -> key option
    34   val defined: 'a table -> key -> bool
    34   val defined: 'a table -> key -> bool
    35   val lookup: 'a table -> key -> 'a option
    35   val lookup: 'a table -> key -> 'a option
    36   val update: (key * 'a) -> 'a table -> 'a table
    36   val update: key * 'a -> 'a table -> 'a table
    37   val update_new: (key * 'a) -> 'a table -> 'a table                   (*exception DUP*)
    37   val update_new: key * 'a -> 'a table -> 'a table                     (*exception DUP*)
    38   val default: key * 'a -> 'a table -> 'a table
    38   val default: key * 'a -> 'a table -> 'a table
    39   val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
    39   val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
    40   val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
    40   val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
    41   val make: (key * 'a) list -> 'a table                                (*exception DUP*)
    41   val make: (key * 'a) list -> 'a table                                (*exception DUP*)
    42   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    42   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    43     'a table * 'a table -> 'a table                                    (*exception DUP*)
    43     'a table * 'a table -> 'a table                                    (*exception DUP*)
    44   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
    44   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
    45   val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
    45   val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
    46   val delete_safe: key -> 'a table -> 'a table
    46   val delete_safe: key -> 'a table -> 'a table
    47   val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
    47   val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
    48   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
    48   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
    49   val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
    49   val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
    50   val lookup_list: 'a list table -> key -> 'a list
    50   val lookup_list: 'a list table -> key -> 'a list
    51   val cons_list: (key * 'a) -> 'a list table -> 'a list table
    51   val cons_list: key * 'a -> 'a list table -> 'a list table
    52   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
    52   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
    53   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
    53   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
    54   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
    54   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
    55   val make_list: (key * 'a) list -> 'a list table
    55   val make_list: (key * 'a) list -> 'a list table
    56   val dest_list: 'a list table -> (key * 'a) list
    56   val dest_list: 'a list table -> (key * 'a) list