--- 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));
--- 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);