# HG changeset patch
# User wenzelm
# Date 1320960730 -3600
# Node ID 41e641a870de7c207849b5b75c204ba756a62685
# Parent  ac069060e08ad7f3a879c27754d4db253c92f5d7
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;

diff -r ac069060e08a -r 41e641a870de src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/General/markup.ML	Thu Nov 10 22:32:10 2011 +0100
@@ -56,6 +56,7 @@
   val typN: string val typ: T
   val termN: string val term: T
   val propN: string val prop: T
+  val typingN: string val typing: T
   val ML_keywordN: string val ML_keyword: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
@@ -250,6 +251,8 @@
 val (termN, term) = markup_elem "term";
 val (propN, prop) = markup_elem "prop";
 
+val (typingN, typing) = markup_elem "typing";
+
 
 (* ML syntax *)
 
diff -r ac069060e08a -r 41e641a870de src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/General/markup.scala	Thu Nov 10 22:32:10 2011 +0100
@@ -123,6 +123,8 @@
   val TERM = "term"
   val PROP = "prop"
 
+  val TYPING = "typing"
+
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
 
diff -r ac069060e08a -r 41e641a870de src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 22:32:10 2011 +0100
@@ -213,11 +213,11 @@
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
-                SOME p => decode (p :: ps) qs bs t
+                SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
               | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
-                SOME q => decode ps (q :: qs) bs t
+                SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
               | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
           | decode _ qs bs (Abs (x, T, t)) =
               let
@@ -794,7 +794,7 @@
 val apply_typ_uncheck = check fst true;
 val apply_term_uncheck = check snd true;
 
-fun prepare_types ctxt tys =
+fun prepare_sorts ctxt tys =
   let
     fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
     val env =
@@ -813,14 +813,26 @@
 in
 
 fun check_typs ctxt =
-  prepare_types ctxt #>
+  prepare_sorts ctxt #>
   apply_typ_check ctxt #>
   Term_Sharing.typs (Proof_Context.theory_of ctxt);
 
-fun check_terms ctxt =
-  Term.burrow_types (prepare_types ctxt) #>
-  apply_term_check ctxt #>
-  Term_Sharing.terms (Proof_Context.theory_of ctxt);
+fun check_terms ctxt raw_ts =
+  let
+    val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts;
+    val tys = map (Logic.mk_type o snd) ps;
+    val (ts', tys') =
+      Term.burrow_types (prepare_sorts ctxt) ts @ tys
+      |> apply_term_check ctxt
+      |> chop (length ts);
+    val _ =
+      map2 (fn (pos, _) => fn ty =>
+        if Position.is_reported pos then
+          Markup.markup (Position.markup pos Markup.typing)
+            (Syntax.string_of_typ ctxt (Logic.dest_type ty))
+        else "") ps tys'
+      |> implode |> Output.report
+  in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
 
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 
diff -r ac069060e08a -r 41e641a870de src/Pure/Syntax/term_position.ML
--- a/src/Pure/Syntax/term_position.ML	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/Syntax/term_position.ML	Thu Nov 10 22:32:10 2011 +0100
@@ -9,7 +9,8 @@
   val pretty: Position.T -> Pretty.T
   val encode: Position.T -> string
   val decode: string -> Position.T option
-  val decode_position: term -> Position.T option
+  val decode_position: term -> (Position.T * typ) option
+  val decode_positionT: typ -> Position.T option
   val is_position: term -> bool
   val strip_positions: term -> term
 end;
@@ -39,9 +40,15 @@
 
 (* positions within parse trees *)
 
-fun decode_position (Free (x, _)) = decode x
+fun decode_position (Free (x, _)) =
+      (case decode x of
+        SOME pos => SOME (pos, TFree (x, dummyS))
+      | NONE => NONE)
   | decode_position _ = NONE;
 
+fun decode_positionT (TFree (x, _)) = decode x
+  | decode_positionT _ = NONE;
+
 val is_position = is_some o decode_position;
 
 fun strip_positions ((t as Const (c, _)) $ u $ v) =
diff -r ac069060e08a -r 41e641a870de src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/type.ML	Thu Nov 10 22:32:10 2011 +0100
@@ -10,6 +10,7 @@
   (*constraints*)
   val mark_polymorphic: typ -> typ
   val constraint: typ -> term -> term
+  val constraint_type: Proof.context -> typ -> typ
   val strip_constraints: term -> term
   val appl_error: Proof.context -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
@@ -110,6 +111,10 @@
   if T = dummyT then t
   else Const ("_type_constraint_", T --> T) $ t;
 
+fun constraint_type ctxt T =
+  let fun err () = error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
+  in (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()) end;
+
 fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t
   | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u
   | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
diff -r ac069060e08a -r 41e641a870de src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/type_infer_context.ML	Thu Nov 10 22:32:10 2011 +0100
@@ -7,6 +7,7 @@
 signature TYPE_INFER_CONTEXT =
 sig
   val const_sorts: bool Config.T
+  val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
   val prepare: Proof.context -> term list -> int * term list
   val infer_types: Proof.context -> term list -> term list
 end;
@@ -82,9 +83,7 @@
 
     fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
           let
-            fun err () =
-              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
-            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
+            val A = Type.constraint_type ctxt T;
             val (A', ps_idx') = prepare_typ A ps_idx;
             val (t', ps_idx'') = prepare t ps_idx';
           in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
@@ -115,6 +114,55 @@
   in (tm', (vparams', params', idx'')) end;
 
 
+(* prepare_positions *)
+
+fun prepare_positions ctxt tms =
+  let
+    val visible = Context_Position.is_visible ctxt;
+
+    fun prepareT (Type (a, Ts)) ps_idx =
+          let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx
+          in (Type (a, Ts'), ps_idx') end
+      | prepareT T (ps, idx) =
+          (case Term_Position.decode_positionT T of
+            SOME pos =>
+              if visible then
+                let val U = Type_Infer.mk_param idx []
+                in (U, ((pos, U) :: ps, idx + 1)) end
+              else (dummyT, (ps, idx))
+          | NONE => (T, (ps, idx)));
+
+    fun prepare (Const ("_type_constraint_", T)) ps_idx =
+          let
+            val A = Type.constraint_type ctxt T;
+            val (A', ps_idx') = prepareT A ps_idx;
+          in (Const ("_type_constraint_", A' --> A'), ps_idx') end
+      | prepare (Const (c, T)) ps_idx =
+          let val (T', ps_idx') = prepareT T ps_idx
+          in (Const (c, T'), ps_idx') end
+      | prepare (Free (x, T)) ps_idx =
+          let val (T', ps_idx') = prepareT T ps_idx
+          in (Free (x, T'), ps_idx') end
+      | prepare (Var (xi, T)) ps_idx =
+          let val (T', ps_idx') = prepareT T ps_idx
+          in (Var (xi, T'), ps_idx') end
+      | prepare (t as Bound _) ps_idx = (t, ps_idx)
+      | prepare (Abs (x, T, t)) ps_idx =
+          let
+            val (T', ps_idx') = prepareT T ps_idx;
+            val (t', ps_idx'') = prepare t ps_idx';
+          in (Abs (x, T', t'), ps_idx'') end
+      | prepare (t $ u) ps_idx =
+          let
+            val (t', ps_idx') = prepare t ps_idx;
+            val (u', ps_idx'') = prepare u ps_idx';
+          in (t' $ u', ps_idx'') end;
+
+    val idx = Type_Infer.param_maxidx_of tms + 1;
+    val (tms', (ps, _)) = fold_map prepare tms ([], idx);
+  in (tms', ps) end;
+
+
 
 (** order-sorted unification of types **)
 
diff -r ac069060e08a -r 41e641a870de src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Thu Nov 10 22:32:10 2011 +0100
@@ -179,12 +179,15 @@
       Markup.ML_SOURCE -> "ML source",
       Markup.DOC_SOURCE -> "document source")
 
+  private def string_of_typing(kind: String, body: XML.Body): String =
+    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
+      margin = Isabelle.Int_Property("tooltip-margin"))
+
   val tooltip: Markup_Tree.Select[String] =
   {
     case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
-    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
-      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
-        margin = Isabelle.Int_Property("tooltip-margin"))
+    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
     case Text.Info(_, XML.Elem(Markup(name, _), _))
     if tooltips.isDefinedAt(name) => tooltips(name)
   }