equal
deleted
inserted
replaced
47 error ("Attempt to merge different versions of ML chunk " ^ quote dup); |
47 error ("Attempt to merge different versions of ML chunk " ^ quote dup); |
48 ); |
48 ); |
49 |
49 |
50 fun declare_chunk name thy = |
50 fun declare_chunk name thy = |
51 (Sign.full_bname thy name, |
51 (Sign.full_bname thy name, |
52 ChunkData.map (snd o NameSpace.bind (Sign.naming_of thy) |
52 ChunkData.map (snd o NameSpace.define (Sign.naming_of thy) |
53 (Binding.name name, ([], stamp ()))) thy |
53 (Binding.name name, ([], stamp ()))) thy |
54 handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name)); |
54 handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name)); |
55 |
55 |
56 fun augment_chunk tok name = |
56 fun augment_chunk tok name = |
57 ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok)))); |
57 ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok)))); |