equal
deleted
inserted
replaced
12 fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup => |
12 fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup => |
13 error ("Attempt to merge different versions of ML chunk " ^ quote dup); |
13 error ("Attempt to merge different versions of ML chunk " ^ quote dup); |
14 ); |
14 ); |
15 |
15 |
16 fun declare_chunk name thy = |
16 fun declare_chunk name thy = |
17 (Sign.full_name thy name, |
17 (Sign.full_bname thy name, |
18 ChunkData.map (NameSpace.extend_table (Sign.naming_of thy) [(name, ([], stamp ()))]) thy |
18 ChunkData.map (snd o NameSpace.bind (Sign.naming_of thy) |
|
19 (Binding.name name, ([], stamp ()))) thy |
19 handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name)); |
20 handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name)); |
20 |
21 |
21 fun augment_chunk tok name = |
22 fun augment_chunk tok name = |
22 ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok)))); |
23 ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok)))); |
23 |
24 |