# HG changeset patch
# User wenzelm
# Date 1459282932 -7200
# Node ID 76b814ccce619e06b6a9ecef35a68aee9124f17d
# Parent  d09d71223e7a7f923c3b4ce4e10ff4a1c60d11e3
tuned messages -- more positions;

diff -r d09d71223e7a -r 76b814ccce61 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Mar 29 21:17:29 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Mar 29 22:22:12 2016 +0200
@@ -135,22 +135,22 @@
 
 fun syn_ext_types type_decls =
   let
-    fun mk_infix sy ty t p1 p2 p3 =
+    fun mk_infix sy ty t p1 p2 p3 range =
       Syntax_Ext.Mfix
         (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
-          ty, t, [p1, p2], p3);
+          ty, t, [p1, p2], p3, Position.set_range range);
 
     fun mfix_of (_, _, NoSyn) = NONE
-      | mfix_of (t, ty, Mixfix (sy, ps, p, _)) =
-          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p))
-      | mfix_of (t, ty, Delimfix (sy, _)) =
-          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000))
-      | mfix_of (t, ty, Infix (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
-      | mfix_of (t, ty, Infixl (sy, p, _)) = SOME (mk_infix sy ty t p (p + 1) p)
-      | mfix_of (t, ty, Infixr (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) p p)
+      | 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, Delimfix (sy, range)) =
+          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, 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 check_args (_, ty, mx) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
+    fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) =
           if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
           else
             error ("Bad number of type constructor arguments in mixfix annotation" ^
@@ -170,29 +170,30 @@
 
 fun syn_ext_consts logical_types const_decls =
   let
-    fun mk_infix sy ty c p1 p2 p3 =
+    fun mk_infix sy ty c p1 p2 p3 range =
       [Syntax_Ext.Mfix
-        (Symbol_Pos.explode0 "op " @ Input.source_explode sy, ty, c, [], 1000),
+        (Symbol_Pos.explode0 "op " @ Input.source_explode sy,
+          ty, c, [], 1000, Position.set_range range),
        Syntax_Ext.Mfix
         (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
-          ty, c, [p1, p2], p3)];
+          ty, c, [p1, p2], p3, Position.set_range range)];
 
     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, _)) =
-          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p)]
-      | mfix_of (c, ty, Delimfix (sy, _)) =
-          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000)]
-      | mfix_of (c, ty, Infix (sy, p, _)) = mk_infix sy ty c (p + 1) (p + 1) p
-      | mfix_of (c, ty, Infixl (sy, p, _)) = mk_infix sy ty c p (p + 1) p
-      | mfix_of (c, ty, Infixr (sy, p, _)) = mk_infix sy ty c (p + 1) p p
-      | mfix_of (c, ty, Binder (sy, p, q, _)) =
+      | 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, Delimfix (sy, range)) =
+          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, 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)) =
           [Syntax_Ext.Mfix
             (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)",
-              binder_typ c ty, (binder_name c), [0, p], q)]
+              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));
 
diff -r d09d71223e7a -r 76b814ccce61 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Tue Mar 29 21:17:29 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Mar 29 22:22:12 2016 +0200
@@ -7,7 +7,7 @@
 signature SYNTAX_EXT =
 sig
   val dddot_indexname: indexname
-  datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int
+  datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
   val typ_to_nonterm: typ -> string
   datatype xsymb =
     Delim of string |
@@ -110,17 +110,15 @@
 
 (** datatype mfix **)
 
-(*Mfix (sy, ty, c, ps, p):
+(*Mfix (sy, ty, c, ps, p, pos):
     sy: rhs of production as symbolic text
     ty: type description of production
     c: head of parse tree
     ps: priorities of arguments in sy
-    p: priority of production*)
+    p: priority of production
+    pos: source position*)
 
-datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int;
-
-fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
-  cat_error msg ("in mixfix annotation " ^ quote (Symbol_Pos.content sy) ^ " for " ^ quote const);
+datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T;
 
 
 (* typ_to_nonterm *)
@@ -189,13 +187,15 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod logical_types (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
   let
     val is_logtype = member (op =) logical_types;
 
+    fun err msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
+
     fun check_pri p =
       if p >= 0 andalso p <= 1000 then ()
-      else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
+      else err ("Precedence " ^ string_of_int p ^ " out of range");
 
     fun blocks_ok [] 0 = true
       | blocks_ok [] _ = false
@@ -206,21 +206,20 @@
 
     fun check_blocks syms =
       if blocks_ok syms 0 then ()
-      else err_in_mfix "Unbalanced block parentheses" mfix;
+      else err "Unbalanced block parentheses";
 
 
     val cons_fst = apfst o cons;
 
     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
-      | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
+      | add_args [] _ _ = err "Too many precedences"
       | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
           cons_fst arg (add_args syms ty ps)
       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
           cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
           cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
-      | add_args (Argument _ :: _) _ _ =
-          err_in_mfix "More arguments than in corresponding type" mfix
+      | add_args (Argument _ :: _) _ _ = err "More arguments than in corresponding type"
       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
 
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
@@ -231,7 +230,7 @@
       | logify_types a = a;
 
 
-    val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
+    val raw_symbs = read_mfix sy handle ERROR msg => err msg;
     val args = filter (fn Argument _ => true | _ => false) raw_symbs;
     val (const', typ', syntax_consts, parse_rules) =
       if not (exists is_index args) then (const, typ, NONE, NONE)
@@ -239,9 +238,9 @@
         let
           val indexed_const =
             if const <> "" then const ^ "_indexed"
-            else err_in_mfix "Missing constant name for indexed syntax" mfix;
+            else err "Missing constant name for indexed syntax";
           val rangeT = Term.range_type typ handle Match =>
-            err_in_mfix "Missing structure argument for indexed syntax" mfix;
+            err "Missing structure argument for indexed syntax";
 
           val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
           val (xs1, xs2) = chop (find_index is_index args) xs;
@@ -268,10 +267,10 @@
 
     val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
     val xprod' =
-      if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
+      if Lexicon.is_terminal lhs' then err ("Illegal lhs " ^ quote lhs')
       else if const <> "" then xprod
       else if length (filter is_argument symbs') <> 1 then
-        err_in_mfix "Copy production must have exactly one argument" mfix
+        err "Copy production must have exactly one argument"
       else if exists is_terminal symbs' then xprod
       else XProd (lhs', map rem_pri symbs', "", chain_pri);