# HG changeset patch
# User wenzelm
# Date 1451311863 -3600
# Node ID 8d996ee7e986e570ecef46bf9dc49c1a6262d91b
# Parent  844881193616ed5ed490bcdc4e5db3e4a3fcfc26
more position information;

diff -r 844881193616 -r 8d996ee7e986 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Dec 27 17:08:31 2015 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Dec 28 15:11:03 2015 +0100
@@ -11,18 +11,20 @@
     term list * Proof.context
   val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
     term * Proof.context
+  val check_free_spec:
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+    ((((binding * typ) * mixfix) list * (Attrib.binding * term) list) * (string -> Position.T))
+      * Proof.context
+  val read_free_spec:
+    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+    ((((binding * typ) * mixfix) list * (Attrib.binding * term) list) * (string -> Position.T))
+      * Proof.context
   val check_spec:
     (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   val read_spec:
     (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
-  val check_free_spec:
-    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
-  val read_free_spec:
-    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   val check_specification: (binding * typ option * mixfix) list ->
     (Attrib.binding * term list) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
@@ -112,6 +114,19 @@
     val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs);
   in map close As end;
 
+fun get_positions ctxt x =
+  let
+    fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
+      | get _ (t $ u) = get [] t @ get [] u
+      | get _ (Abs (_, _, t)) = get [] t
+      | get Cs (Free (y, T)) =
+          if x = y then
+            map_filter Term_Position.decode_positionT
+              (T :: map (Type.constraint_type ctxt) Cs)
+          else []
+      | get _ _ = [];
+  in get [] end;
+
 fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
     val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
@@ -124,6 +139,7 @@
       |> fold Name.declare xs;
     val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
     val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1;
+
     val specs =
       (if do_close then
         #1 (fold_map
@@ -134,8 +150,16 @@
 
     val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
     val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
-    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
-  in ((params, name_atts ~~ specs), specs_ctxt) end;
+    val name_atts: Attrib.binding list =
+      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
+
+    fun get_pos x =
+      if do_close then Position.none
+      else
+        (case (maps o maps o maps) (get_positions specs_ctxt x) Asss' of
+          [] => Position.none
+        | pos :: _ => pos);
+  in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
 
 
 fun single_spec (a, prop) = [(a, [prop])];
@@ -143,21 +167,27 @@
 
 fun prep_spec prep_var parse_prop prep_att do_close vars specs =
   prepare prep_var parse_prop prep_att do_close
-    vars (map single_spec specs) #>> apsnd (map the_spec);
+    vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
 
 in
 
-fun check_spec x = prep_spec Proof_Context.cert_var (K I) (K I) true x;
-fun read_spec x = prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src true x;
+fun check_free_spec vars specs =
+  prep_spec Proof_Context.cert_var (K I) (K I) false vars specs;
+
+fun read_free_spec vars specs =
+  prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src false vars specs;
 
-fun check_free_spec x = prep_spec Proof_Context.cert_var (K I) (K I) false x;
-fun read_free_spec x = prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src false x;
+fun check_spec vars specs =
+  prep_spec Proof_Context.cert_var (K I) (K I) true vars specs #> apfst fst;
+
+fun read_spec vars specs =
+  prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars specs #> apfst fst;
 
 fun check_specification vars specs =
-  prepare Proof_Context.cert_var (K I) (K I) true vars [specs];
+  prepare Proof_Context.cert_var (K I) (K I) true vars [specs] #> apfst fst
 
 fun read_specification vars specs =
-  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars [specs];
+  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars [specs] #> apfst fst;
 
 end;
 
@@ -198,12 +228,13 @@
 
 fun gen_def prep (raw_var, raw_spec) int lthy =
   let
-    val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
+    val ((vars, [((raw_name, atts), prop)]), get_pos) =
+      fst (prep (the_list raw_var) [raw_spec] lthy);
     val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
     val _ = Name.reject_internal (x, []);
     val var as (b, _) =
       (case vars of
-        [] => (Binding.name x, NoSyn)
+        [] => (Binding.make (x, get_pos x), NoSyn)
       | [((b, _), mx)] =>
           let
             val y = Variable.check_name b;
@@ -239,14 +270,14 @@
   let
     val lthy1 = lthy
       |> Proof_Context.set_syntax_mode mode;
-    val ((vars, [(_, prop)]), _) =
+    val (((vars, [(_, prop)]), get_pos), _) =
       prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
         (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
     val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
     val _ = Name.reject_internal (x, []);
     val var =
       (case vars of
-        [] => (Binding.name x, NoSyn)
+        [] => (Binding.make (x, get_pos x), NoSyn)
       | [((b, _), mx)] =>
           let
             val y = Variable.check_name b;