18 |
18 |
19 fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind); |
19 fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind); |
20 |
20 |
21 structure Data = Theory_Data |
21 structure Data = Theory_Data |
22 ( |
22 ( |
23 type T = ((theory -> Name_Space.T) * serial) Symtab.table; |
23 type T = (theory -> Name_Space.T) Inttab.table; |
24 val empty = Symtab.empty; |
24 val empty = Inttab.empty; |
25 val extend = I; |
25 val extend = I; |
26 fun merge data = |
26 val merge = Inttab.merge (K true); |
27 Symtab.merge (eq_snd op =) data |
|
28 handle Symtab.DUP dup => err_dup_kind dup; |
|
29 ); |
27 ); |
30 |
28 |
31 val other_name_spaces = map (#1 o #2) o Symtab.dest o Data.get; |
29 val other_name_spaces = map #2 o Inttab.dest o Data.get; |
32 |
30 fun other_name_space get_space thy = Data.map (Inttab.update (serial (), get_space)) thy; |
33 fun other_name_space get_space thy = |
|
34 let |
|
35 val kind = Name_Space.kind_of (get_space thy); |
|
36 val entry = (get_space, serial ()); |
|
37 in |
|
38 Data.map (Symtab.update_new (kind, entry)) thy |
|
39 handle Symtab.DUP dup => err_dup_kind dup |
|
40 end; |
|
41 |
31 |
42 val _ = Theory.setup |
32 val _ = Theory.setup |
43 (other_name_space Thm.oracle_space #> |
33 (other_name_space Thm.oracle_space #> |
44 other_name_space Global_Theory.fact_space #> |
34 other_name_space Global_Theory.fact_space #> |
45 other_name_space (Bundle.bundle_space o Context.Theory) #> |
35 other_name_space (Bundle.bundle_space o Context.Theory) #> |