equal
deleted
inserted
replaced
17 (* style data *) |
17 (* style data *) |
18 |
18 |
19 fun err_dup_style name = |
19 fun err_dup_style name = |
20 error ("Duplicate declaration of antiquote style: " ^ quote name); |
20 error ("Duplicate declaration of antiquote style: " ^ quote name); |
21 |
21 |
22 structure StyleData = TheoryDataFun |
22 structure StyleData = Theory_Data |
23 ( |
23 ( |
24 type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table; |
24 type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table; |
25 val empty = Symtab.empty; |
25 val empty = Symtab.empty; |
26 val copy = I; |
|
27 val extend = I; |
26 val extend = I; |
28 fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs |
27 fun merge data : T = Symtab.merge (eq_snd (op =)) data |
29 handle Symtab.DUP dup => err_dup_style dup; |
28 handle Symtab.DUP dup => err_dup_style dup; |
30 ); |
29 ); |
31 |
30 |
32 |
31 |
33 (* accessors *) |
32 (* accessors *) |