more operations;
authorwenzelm
Sun May 13 15:05:21 2018 +0200 (12 months ago)
changeset 68163b168f30e541f
parent 68160 efce008331f6
child 68164 738071699826
more operations;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sun May 13 13:43:34 2018 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sun May 13 15:05:21 2018 +0200
     1.3 @@ -62,6 +62,7 @@
     1.4    val alias: naming -> binding -> string -> T -> T
     1.5    val naming_of: Context.generic -> naming
     1.6    val map_naming: (naming -> naming) -> Context.generic -> Context.generic
     1.7 +  val declared: T -> string -> bool
     1.8    val declare: Context.generic -> bool -> binding -> T -> string * T
     1.9    type 'a table
    1.10    val change_base: bool -> 'a table -> 'a table
    1.11 @@ -80,6 +81,7 @@
    1.12    val del_table: string -> 'a table -> 'a table
    1.13    val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
    1.14    val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
    1.15 +  val dest_table: 'a table -> (string * 'a) list
    1.16    val empty_table: string -> 'a table
    1.17    val merge_tables: 'a table * 'a table -> 'a table
    1.18    val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
    1.19 @@ -503,6 +505,8 @@
    1.20  
    1.21  (* declaration *)
    1.22  
    1.23 +fun declared (Name_Space {entries, ...}) = Change_Table.defined entries;
    1.24 +
    1.25  fun declare context strict binding space =
    1.26    let
    1.27      val naming = naming_of context;
    1.28 @@ -608,6 +612,7 @@
    1.29    Table (space, Change_Table.map_entry name f tab);
    1.30  
    1.31  fun fold_table f (Table (_, tab)) = Change_Table.fold f tab;
    1.32 +fun dest_table (Table (_, tab)) = Change_Table.dest tab;
    1.33  
    1.34  fun empty_table kind = Table (empty kind, Change_Table.empty);
    1.35