src/Pure/Syntax/mixfix.ML
changeset 62753 76b814ccce61
parent 62752 d09d71223e7a
child 62759 d16b2ec535ba
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Mar 29 21:17:29 2016 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Mar 29 22:22:12 2016 +0200
     1.3 @@ -135,22 +135,22 @@
     1.4  
     1.5  fun syn_ext_types type_decls =
     1.6    let
     1.7 -    fun mk_infix sy ty t p1 p2 p3 =
     1.8 +    fun mk_infix sy ty t p1 p2 p3 range =
     1.9        Syntax_Ext.Mfix
    1.10          (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
    1.11 -          ty, t, [p1, p2], p3);
    1.12 +          ty, t, [p1, p2], p3, Position.set_range range);
    1.13  
    1.14      fun mfix_of (_, _, NoSyn) = NONE
    1.15 -      | mfix_of (t, ty, Mixfix (sy, ps, p, _)) =
    1.16 -          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p))
    1.17 -      | mfix_of (t, ty, Delimfix (sy, _)) =
    1.18 -          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000))
    1.19 -      | mfix_of (t, ty, Infix (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
    1.20 -      | mfix_of (t, ty, Infixl (sy, p, _)) = SOME (mk_infix sy ty t p (p + 1) p)
    1.21 -      | mfix_of (t, ty, Infixr (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) p p)
    1.22 +      | mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
    1.23 +          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
    1.24 +      | mfix_of (t, ty, Delimfix (sy, range)) =
    1.25 +          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, Position.set_range range))
    1.26 +      | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
    1.27 +      | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
    1.28 +      | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
    1.29        | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
    1.30  
    1.31 -    fun check_args (_, ty, mx) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
    1.32 +    fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) =
    1.33            if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
    1.34            else
    1.35              error ("Bad number of type constructor arguments in mixfix annotation" ^
    1.36 @@ -170,29 +170,30 @@
    1.37  
    1.38  fun syn_ext_consts logical_types const_decls =
    1.39    let
    1.40 -    fun mk_infix sy ty c p1 p2 p3 =
    1.41 +    fun mk_infix sy ty c p1 p2 p3 range =
    1.42        [Syntax_Ext.Mfix
    1.43 -        (Symbol_Pos.explode0 "op " @ Input.source_explode sy, ty, c, [], 1000),
    1.44 +        (Symbol_Pos.explode0 "op " @ Input.source_explode sy,
    1.45 +          ty, c, [], 1000, Position.set_range range),
    1.46         Syntax_Ext.Mfix
    1.47          (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
    1.48 -          ty, c, [p1, p2], p3)];
    1.49 +          ty, c, [p1, p2], p3, Position.set_range range)];
    1.50  
    1.51      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    1.52            [Type ("idts", []), ty2] ---> ty3
    1.53        | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
    1.54  
    1.55      fun mfix_of (_, _, NoSyn) = []
    1.56 -      | mfix_of (c, ty, Mixfix (sy, ps, p, _)) =
    1.57 -          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p)]
    1.58 -      | mfix_of (c, ty, Delimfix (sy, _)) =
    1.59 -          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000)]
    1.60 -      | mfix_of (c, ty, Infix (sy, p, _)) = mk_infix sy ty c (p + 1) (p + 1) p
    1.61 -      | mfix_of (c, ty, Infixl (sy, p, _)) = mk_infix sy ty c p (p + 1) p
    1.62 -      | mfix_of (c, ty, Infixr (sy, p, _)) = mk_infix sy ty c (p + 1) p p
    1.63 -      | mfix_of (c, ty, Binder (sy, p, q, _)) =
    1.64 +      | mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
    1.65 +          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
    1.66 +      | mfix_of (c, ty, Delimfix (sy, range)) =
    1.67 +          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, Position.set_range range)]
    1.68 +      | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
    1.69 +      | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
    1.70 +      | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range
    1.71 +      | mfix_of (c, ty, Binder (sy, p, q, range)) =
    1.72            [Syntax_Ext.Mfix
    1.73              (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)",
    1.74 -              binder_typ c ty, (binder_name c), [0, p], q)]
    1.75 +              binder_typ c ty, (binder_name c), [0, p], q, Position.set_range range)]
    1.76        | mfix_of (c, _, mx) =
    1.77            error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx));
    1.78