src/Pure/Syntax/mixfix.ML
changeset 62796 99f2036f37af
parent 62773 e6443edaebff
child 62797 e08c44eed27f
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 01 17:14:27 2016 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 01 17:23:15 2016 +0200
     1.3 @@ -125,18 +125,20 @@
     1.4  
     1.5  fun syn_ext_types type_decls =
     1.6    let
     1.7 -    fun mk_infix sy ty t p1 p2 p3 range =
     1.8 +    fun mk_infix sy ty t p1 p2 p3 pos =
     1.9        Syntax_Ext.Mfix
    1.10          (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
    1.11 -          ty, t, [p1, p2], p3, Position.set_range range);
    1.12 +          ty, t, [p1, p2], p3, pos);
    1.13  
    1.14 -    fun mfix_of (_, _, NoSyn) = NONE
    1.15 -      | mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
    1.16 -          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
    1.17 -      | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
    1.18 -      | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
    1.19 -      | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
    1.20 -      | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
    1.21 +    fun mfix_of (mfix as (_, _, mx)) =
    1.22 +      (case mfix of
    1.23 +        (_, _, NoSyn) => NONE
    1.24 +      | (t, ty, Mixfix (sy, ps, p, _)) =>
    1.25 +          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, pos_of mx))
    1.26 +      | (t, ty, Infix (sy, p, _)) => SOME (mk_infix sy ty t (p + 1) (p + 1) p (pos_of mx))
    1.27 +      | (t, ty, Infixl (sy, p, _)) => SOME (mk_infix sy ty t p (p + 1) p (pos_of mx))
    1.28 +      | (t, ty, Infixr (sy, p, _)) => SOME (mk_infix sy ty t (p + 1) p p (pos_of mx))
    1.29 +      | (t, _, _) => error ("Bad mixfix declaration for " ^ quote t ^ Position.here (pos_of mx)));
    1.30  
    1.31      fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) =
    1.32            if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
    1.33 @@ -158,30 +160,32 @@
    1.34  
    1.35  fun syn_ext_consts logical_types const_decls =
    1.36    let
    1.37 -    fun mk_infix sy ty c p1 p2 p3 range =
    1.38 +    fun mk_infix sy ty c p1 p2 p3 pos =
    1.39        [Syntax_Ext.Mfix
    1.40          (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
    1.41            ty, c, [], 1000, Position.none),
    1.42         Syntax_Ext.Mfix
    1.43          (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
    1.44 -          ty, c, [p1, p2], p3, Position.set_range range)];
    1.45 +          ty, c, [p1, p2], p3, pos)];
    1.46  
    1.47      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    1.48            [Type ("idts", []), ty2] ---> ty3
    1.49        | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
    1.50  
    1.51 -    fun mfix_of (_, _, NoSyn) = []
    1.52 -      | mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
    1.53 -          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
    1.54 -      | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
    1.55 -      | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
    1.56 -      | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range
    1.57 -      | mfix_of (c, ty, Binder (sy, p, q, range)) =
    1.58 +    fun mfix_of (mfix as (_, _, mx)) =
    1.59 +      (case mfix of
    1.60 +        (_, _, NoSyn) => []
    1.61 +      | (c, ty, Mixfix (sy, ps, p, _)) =>
    1.62 +          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)]
    1.63 +      | (c, ty, Infix (sy, p, _)) => mk_infix sy ty c (p + 1) (p + 1) p (pos_of mx)
    1.64 +      | (c, ty, Infixl (sy, p, _)) => mk_infix sy ty c p (p + 1) p (pos_of mx)
    1.65 +      | (c, ty, Infixr (sy, p, _)) => mk_infix sy ty c (p + 1) p p (pos_of mx)
    1.66 +      | (c, ty, Binder (sy, p, q, _)) =>
    1.67            [Syntax_Ext.Mfix
    1.68              (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)",
    1.69 -              binder_typ c ty, (binder_name c), [0, p], q, Position.set_range range)]
    1.70 -      | mfix_of (c, _, mx) =
    1.71 -          error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx));
    1.72 +              binder_typ c ty, (binder_name c), [0, p], q, pos_of mx)]
    1.73 +      | (c, _, mx) =>
    1.74 +          error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx)));
    1.75  
    1.76      fun binder (c, _, Binder _) = SOME (binder_name c, c)
    1.77        | binder _ = NONE;