# HG changeset patch
# User wenzelm
# Date 1467721227 -7200
# Node ID 734723445a8cc1a617d9cca15954a62810b48f45
# Parent  7faeff3156d5cadffabdaa8cf486c17970ea84cf
PIDE reports of implicit variable scope;

diff -r 7faeff3156d5 -r 734723445a8c src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -572,7 +572,7 @@
     val forced_rhs = force_rty_type lthy rty_forced rhs
     val lhs = Free (Binding.name_of binding, qty)
     val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
-    val (_, prop') = Local_Defs.cert_def lthy prop
+    val (_, prop') = Local_Defs.cert_def lthy (K []) prop
     val (_, newrhs) = Local_Defs.abs_def prop'
     val var = ((#notes config = false ? Binding.concealed) binding, mx)
     val def_name = Thm.make_def_binding (#notes config) (#1 var)
diff -r 7faeff3156d5 -r 734723445a8c src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -96,7 +96,8 @@
         (Binding.empty_atts, definition_term) lthy |>> (snd #> snd);
     fun raw_def lthy =
       let
-        val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
+        val ((_, rhs), prove) =
+          Local_Defs.derived_def lthy (K []) {conditional = true} definition_term;
         val ((_, (_, raw_th)), lthy) =
           Local_Theory.define
             ((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy;
diff -r 7faeff3156d5 -r 734723445a8c src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -58,7 +58,7 @@
     val absrep_trm =
       Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
     val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
-    val (_, prop') = Local_Defs.cert_def lthy prop
+    val (_, prop') = Local_Defs.cert_def lthy (K []) prop
     val (_, newrhs) = Local_Defs.abs_def prop'
 
     val ((trm, (_ , def_thm)), lthy') =
diff -r 7faeff3156d5 -r 734723445a8c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -1039,7 +1039,7 @@
         let
           val _ = Binding.is_empty name andalso null atts orelse
             error "Abbreviations may not have names or attributes";
-          val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
+          val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 (K []) t));
           val var =
             (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
               NONE => error ("Undeclared head of abbreviation " ^ quote x)
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/element.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -492,7 +492,7 @@
       let
         val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
         val asms = defs' |> map (fn (b, (t, ps)) =>
-            let val (_, t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
+            let val (_, t') = Local_Defs.cert_def ctxt (K []) t  (* FIXME adapt ps? *)
             in (t', (b, [(t', ps)])) end);
         val (_, ctxt') = ctxt
           |> fold Variable.auto_fixes (map #1 asms)
@@ -517,7 +517,8 @@
       (case (map_ctxt_attrib o map) Token.init_assignable elem of
         Defines defs =>
           Defines (defs |> map (fn ((a, atts), (t, ps)) =>
-            ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
+            ((Thm.def_binding_optional
+              (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
               (t, ps))))
       | e => e);
     val ctxt' = Context.proof_map (init elem') ctxt;
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -330,7 +330,7 @@
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
-            let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
+            let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t)
             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
@@ -540,7 +540,7 @@
 
 fun bind_def ctxt eq (xs, env, eqs) =
   let
-    val _ = Local_Defs.cert_def ctxt eq;
+    val _ = Local_Defs.cert_def ctxt (K []) eq;
     val ((y, T), b) = Local_Defs.abs_def eq;
     val b' = norm_term env b;
     fun err msg = error (msg ^ ": " ^ quote y);
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -6,7 +6,7 @@
 
 signature LOCAL_DEFS =
 sig
-  val cert_def: Proof.context -> term -> (string * typ) * term
+  val cert_def: Proof.context -> (string -> Position.T list) -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
@@ -33,8 +33,8 @@
   val unfold0_tac: Proof.context -> thm list -> tactic
   val fold: Proof.context -> thm list -> thm -> thm
   val fold_tac: Proof.context -> thm list -> tactic
-  val derived_def: Proof.context -> {conditional: bool} -> term ->
-    ((string * typ) * term) * (Proof.context -> thm -> thm)
+  val derived_def: Proof.context -> (string -> Position.T list) -> {conditional: bool} ->
+    term -> ((string * typ) * term) * (Proof.context -> thm -> thm)
 end;
 
 structure Local_Defs: LOCAL_DEFS =
@@ -44,12 +44,12 @@
 
 (* prepare defs *)
 
-fun cert_def ctxt eq =
+fun cert_def ctxt get_pos eq =
   let
     fun err msg =
       cat_error msg ("The error(s) above occurred in definition:\n" ^
         quote (Syntax.string_of_term ctxt eq));
-    val ((lhs, _), eq') = eq
+    val ((lhs, _), args, eq') = eq
       |> Sign.no_vars ctxt
       |> Primitive_Defs.dest_def ctxt
         {check_head = Term.is_Free,
@@ -57,6 +57,9 @@
          check_free_rhs = if Variable.is_body ctxt then K true else Variable.is_fixed ctxt,
          check_tfree = K true}
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
+    val _ =
+      Context_Position.reports ctxt
+        (maps (fn Free (x, _) => Syntax_Phases.reports_of_scope (get_pos x) | _ => []) args);
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
 val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free;
@@ -121,7 +124,7 @@
       |> Variable.declare_term rhs
       |> Proof_Context.add_fixes [(x, SOME T, mx)];
     val lhs = Free (x', T);
-    val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
+    val _ = cert_def ctxt' (K []) (Logic.mk_equals (lhs, rhs));
     fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
     val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
   in ((lhs, rhs), ctxt'') end;
@@ -240,14 +243,14 @@
 
 (* derived defs -- potentially within the object-logic *)
 
-fun derived_def ctxt {conditional} prop =
+fun derived_def ctxt get_pos {conditional} prop =
   let
     val ((c, T), rhs) = prop
       |> Thm.cterm_of ctxt
       |> meta_rewrite_conv ctxt
       |> (snd o Logic.dest_equals o Thm.prop_of)
       |> conditional ? Logic.strip_imp_concl
-      |> (abs_def o #2 o cert_def ctxt);
+      |> (abs_def o #2 o cert_def ctxt get_pos);
     fun prove ctxt' def =
       Goal.prove ctxt'
         ((not (Variable.is_body ctxt') ? Variable.add_free_names ctxt' prop) []) [] prop
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -862,7 +862,7 @@
             (if null more_decls then "" else " ") ^
             "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs));
 
-    val derived_def = Local_Defs.derived_def ctxt {conditional = false};
+    val derived_def = Local_Defs.derived_def ctxt (K  []) {conditional = false};
     val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
     val defs2 = match_defs decls defs1;
     val (defs3, defs_ctxt) = Local_Defs.define defs2 ctxt;
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -11,11 +11,11 @@
     term list * Proof.context
   val check_spec_open: (binding * typ option * mixfix) list ->
     (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
-    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+    ((binding * typ option * mixfix) list * string list * (string -> Position.T list) * term) *
     Proof.context
   val read_spec_open: (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list -> string list -> string -> Proof.context ->
-    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+    ((binding * typ option * mixfix) list * string list * (string -> Position.T list) * term) *
     Proof.context
   type multi_specs =
     ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list
@@ -146,10 +146,7 @@
     val spec = Logic.list_implies (prems, concl);
     val spec_ctxt = Variable.declare_term spec params_ctxt;
 
-    fun get_pos x =
-      (case maps (get_positions spec_ctxt x) props of
-        [] => Position.none
-      | pos :: _ => pos);
+    fun get_pos x = maps (get_positions spec_ctxt x) props;
   in ((vars, xs, get_pos, spec), spec_ctxt) end;
 
 fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt =
@@ -242,11 +239,11 @@
 
     val ((vars, xs, get_pos, spec), _) = lthy
       |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
-    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
+    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = true} spec;
     val _ = Name.reject_internal (x, []);
     val (b, mx) =
       (case (vars, xs) of
-        ([], []) => (Binding.make (x, get_pos x), NoSyn)
+        ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn)
       | ([(b, _, mx)], [y]) =>
           if x = y then (b, mx)
           else
@@ -282,11 +279,11 @@
     val ((vars, xs, get_pos, spec), _) = lthy
       |> Proof_Context.set_mode Proof_Context.mode_abbrev
       |> prep_spec (the_list raw_var) raw_params [] raw_spec;
-    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));
+    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 get_pos spec));
     val _ = Name.reject_internal (x, []);
     val (b, mx) =
       (case (vars, xs) of
-        ([], []) => (Binding.make (x, get_pos x), NoSyn)
+        ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn)
       | ([(b, _, mx)], [y]) =>
           if x = y then (b, mx)
           else
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -7,6 +7,7 @@
 
 signature SYNTAX_PHASES =
 sig
+  val reports_of_scope: Position.T list -> Position.report list
   val decode_sort: term -> sort
   val decode_typ: term -> typ
   val decode_term: Proof.context ->
@@ -77,6 +78,20 @@
 
 
 
+(** reports of implicit variable scope **)
+
+fun reports_of_scope [] = []
+  | reports_of_scope (def_pos :: ps) =
+      let
+        val id = serial ();
+        fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos);
+      in
+        map (rpair Markup.bound) (def_pos :: ps) @
+        ((def_pos, entity true) :: map (rpair (entity false)) ps)
+      end;
+
+
+
 (** decode parse trees **)
 
 (* decode_sort *)
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/primitive_defs.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -11,7 +11,7 @@
      check_free_lhs: string -> bool,
      check_free_rhs: string -> bool,
      check_tfree: string -> bool} ->
-    term -> (term * term) * term
+    term -> (term * term) * term list * term
   val abs_def: term -> term * term
 end;
 
@@ -68,7 +68,8 @@
     else if exists_subterm (fn t => t aconv head) rhs then
       err "Entity to be defined occurs on rhs"
     else
-      ((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
+      ((lhs, rhs), args,
+        fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
   end;
 
 (*!!x. c x == t[x] to c == %x. t[x]*)
diff -r 7faeff3156d5 -r 734723445a8c src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/theory.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -291,7 +291,7 @@
 fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
   let
     val name = Sign.full_name thy b;
-    val ((lhs, rhs), _) =
+    val ((lhs, rhs), _, _) =
       Primitive_Defs.dest_def ctxt
         {check_head = Term.is_Const,
          check_free_lhs = K true,