# HG changeset patch # User wenzelm # Date 1459524195 -7200 # Node ID 99f2036f37afc1595eaa01d5eafdcea646a7cf72 # Parent 063d2f23cdf64f2302b9d4282c3ce71ccd94d99b tuned; diff -r 063d2f23cdf6 -r 99f2036f37af src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri Apr 01 17:14:27 2016 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri Apr 01 17:23:15 2016 +0200 @@ -125,18 +125,20 @@ fun syn_ext_types type_decls = let - fun mk_infix sy ty t p1 p2 p3 range = + fun mk_infix sy ty t p1 p2 p3 pos = Syntax_Ext.Mfix (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", - ty, t, [p1, p2], p3, Position.set_range range); + ty, t, [p1, p2], p3, pos); - fun mfix_of (_, _, NoSyn) = NONE - | mfix_of (t, ty, Mixfix (sy, ps, p, range)) = - SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range)) - | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range) - | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range) - | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range) - | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); + fun mfix_of (mfix as (_, _, mx)) = + (case mfix of + (_, _, NoSyn) => NONE + | (t, ty, Mixfix (sy, ps, p, _)) => + SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, pos_of mx)) + | (t, ty, Infix (sy, p, _)) => SOME (mk_infix sy ty t (p + 1) (p + 1) p (pos_of mx)) + | (t, ty, Infixl (sy, p, _)) => SOME (mk_infix sy ty t p (p + 1) p (pos_of mx)) + | (t, ty, Infixr (sy, p, _)) => SOME (mk_infix sy ty t (p + 1) p p (pos_of mx)) + | (t, _, _) => error ("Bad mixfix declaration for " ^ quote t ^ Position.here (pos_of mx))); fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) = if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then () @@ -158,30 +160,32 @@ fun syn_ext_consts logical_types const_decls = let - fun mk_infix sy ty c p1 p2 p3 range = + fun mk_infix sy ty c p1 p2 p3 pos = [Syntax_Ext.Mfix (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy), ty, c, [], 1000, Position.none), Syntax_Ext.Mfix (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", - ty, c, [p1, p2], p3, Position.set_range range)]; + ty, c, [p1, p2], p3, pos)]; fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = [Type ("idts", []), ty2] ---> ty3 | binder_typ c _ = error ("Bad type of binder: " ^ quote c); - fun mfix_of (_, _, NoSyn) = [] - | mfix_of (c, ty, Mixfix (sy, ps, p, range)) = - [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)] - | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range - | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range - | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range - | mfix_of (c, ty, Binder (sy, p, q, range)) = + fun mfix_of (mfix as (_, _, mx)) = + (case mfix of + (_, _, NoSyn) => [] + | (c, ty, Mixfix (sy, ps, p, _)) => + [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)] + | (c, ty, Infix (sy, p, _)) => mk_infix sy ty c (p + 1) (p + 1) p (pos_of mx) + | (c, ty, Infixl (sy, p, _)) => mk_infix sy ty c p (p + 1) p (pos_of mx) + | (c, ty, Infixr (sy, p, _)) => mk_infix sy ty c (p + 1) p p (pos_of mx) + | (c, ty, Binder (sy, p, q, _)) => [Syntax_Ext.Mfix (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)", - binder_typ c ty, (binder_name c), [0, p], q, Position.set_range range)] - | mfix_of (c, _, mx) = - error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx)); + binder_typ c ty, (binder_name c), [0, p], q, pos_of mx)] + | (c, _, mx) => + error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx))); fun binder (c, _, Binder _) = SOME (binder_name c, c) | binder _ = NONE;