81 | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) |
81 | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) |
82 | prep_mixfix add mode (Fixed, (x, T, mx)) = |
82 | prep_mixfix add mode (Fixed, (x, T, mx)) = |
83 SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); |
83 SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); |
84 |
84 |
85 fun prep_struct (Fixed, (c, _, Structure _)) = SOME c |
85 fun prep_struct (Fixed, (c, _, Structure _)) = SOME c |
86 | prep_struct (_, (c, _, mx as Structure _)) = |
86 | prep_struct (_, (c, _, Structure _)) = error ("Bad structure mixfix declaration for " ^ quote c) |
87 error ("Bad mixfix declaration for " ^ quote c ^ Position.here (Mixfix.pos_of mx)) |
|
88 | prep_struct _ = NONE; |
87 | prep_struct _ = NONE; |
89 |
88 |
90 in |
89 in |
91 |
90 |
92 fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) = |
91 fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) = |