59 | update_gram ((false, add, m), decls) = |
59 | update_gram ((false, add, m), decls) = |
60 Syntax.update_const_gram add (Sign.is_logtype thy) m decls; |
60 Syntax.update_const_gram add (Sign.is_logtype thy) m decls; |
61 |
61 |
62 val local_syntax = thy_syntax |
62 val local_syntax = thy_syntax |
63 |> Syntax.update_trfuns |
63 |> Syntax.update_trfuns |
64 ([], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_parse_translation structs), |
64 ([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)], |
65 [], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_print_ast_translation structs)) |
65 [], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)]) |
66 |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); |
66 |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); |
67 in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; |
67 in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; |
68 |
68 |
69 fun init thy = build_syntax thy Syntax.mode_default [] ([], []); |
69 fun init thy = build_syntax thy Syntax.mode_default [] ([], []); |
70 |
70 |