relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
--- a/src/Pure/Isar/generic_target.ML Wed Mar 30 20:35:35 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Mar 30 20:56:39 2016 +0200
@@ -98,30 +98,21 @@
in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
fun check_mixfix ctxt (b, extra_tfrees) mx =
- let
- val visible = Context_Position.is_visible ctxt;
- val _ =
- ctxt |> Proof_Context.add_fixes
- [(Binding.reset_pos b, NONE, if visible then mx else Mixfix.reset_pos mx)];
- val mx' =
- if null extra_tfrees then mx
- else
- (if visible then
- warning
- ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
- commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
- (if Mixfix.is_empty mx then ""
- else
- "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
- Position.here (Mixfix.pos_of mx)))
- else (); NoSyn);
- in Mixfix.reset_pos mx' end;
+ if null extra_tfrees then mx
+ else
+ (if Context_Position.is_visible ctxt then
+ warning
+ ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
+ (if Mixfix.is_empty mx then ""
+ else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
+ else (); NoSyn);
fun check_mixfix_global (b, no_params) mx =
if no_params orelse Mixfix.is_empty mx then mx
else
(warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
- Pretty.string_of (Mixfix.pretty_mixfix mx) ^ Position.here (Mixfix.pos_of mx)); NoSyn);
+ Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
fun same_const (Const (c, _), Const (c', _)) = c = c'
| same_const (t $ _, t' $ _) = same_const (t, t')
--- a/src/Pure/Isar/proof_context.ML Wed Mar 30 20:35:35 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 30 20:56:39 2016 +0200
@@ -1062,6 +1062,9 @@
let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
+fun add_syntax vars ctxt =
+ map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt;
+
fun check_var internal b =
let
val x = Variable.check_name b;
@@ -1073,6 +1076,14 @@
local
+fun check_mixfix ctxt (b, opt_T, mx) =
+ let
+ val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
+ val mx' = Mixfix.reset_pos mx;
+ val T = #2 (#1 (declare_var (x, opt_T, mx') ctxt));
+ val _ = add_syntax [(x, T, if Context_Position.is_visible ctxt then mx else mx')] ctxt';
+ in mx' end;
+
fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
let
val x = check_var internal b;
@@ -1080,8 +1091,9 @@
if internal then T
else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
- val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
- in ((b, opt_T, mx), ctxt') end;
+ val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt (b, opt_T, mx);
+ val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx');
+ in ((b, opt_T, mx'), ctxt') end;
in
@@ -1185,7 +1197,7 @@
in
ctxt'
|> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
- |-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
+ |-> add_syntax
|> pair xs
end;