equal
deleted
inserted
replaced
289 fun mfix_to_xprod ctxt logical_types (Mfix (sy, typ, const, pris, pri, pos)) = |
289 fun mfix_to_xprod ctxt logical_types (Mfix (sy, typ, const, pris, pri, pos)) = |
290 let |
290 let |
291 val nonterm_for_lhs = the_default "logic" o try dest_Type_name; |
291 val nonterm_for_lhs = the_default "logic" o try dest_Type_name; |
292 val nonterm_for_rhs = the_default "any" o try dest_Type_name; |
292 val nonterm_for_rhs = the_default "any" o try dest_Type_name; |
293 |
293 |
294 val _ = Position.report pos Markup.language_mixfix; |
294 val _ = Context_Position.report ctxt pos Markup.language_mixfix; |
295 val symbs0 = read_mfix ctxt sy; |
295 val symbs0 = read_mfix ctxt sy; |
296 |
296 |
297 fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos); |
297 fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos); |
298 |
298 |
299 fun check_blocks [] pending bad = pending @ bad |
299 fun check_blocks [] pending bad = pending @ bad |