# HG changeset patch
# User wenzelm
# Date 1301241311 -7200
# Node ID 1d9710ff72097f809499b046f1c556e94aa1a752
# Parent  e10e2cce85c8f06cfa40e37ba3f3819c6ee52d66
decode_term/disambig: report resolved term variables for the unique (!) result;

diff -r e10e2cce85c8 -r 1d9710ff7209 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 27 15:01:47 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 27 17:55:11 2011 +0200
@@ -65,7 +65,7 @@
   val allow_dummies: Proof.context -> Proof.context
   val check_tvar: Proof.context -> indexname * sort -> indexname * sort
   val check_tfree: Proof.context -> string * sort -> string * sort
-  val decode_term: Proof.context -> term -> term
+  val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term
   val standard_infer_types: Proof.context -> term list -> term list
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
diff -r e10e2cce85c8 -r 1d9710ff7209 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Mar 27 15:01:47 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Mar 27 17:55:11 2011 +0200
@@ -756,22 +756,25 @@
 
 (* read terms *)
 
+fun report_result ctxt (reports, res) =
+  (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res);
+
 (*brute-force disambiguation via type-inference*)
-fun disambig _ _ [t] = t
-  | disambig ctxt check ts =
+fun disambig ctxt _ [arg] = report_result ctxt arg
+  | disambig ctxt check args =
       let
         val level = Config.get ctxt ambiguity_level;
         val limit = Config.get ctxt ambiguity_limit;
 
-        val ambiguity = length ts;
+        val ambiguity = length args;
         fun ambig_msg () =
           if ambiguity > 1 andalso ambiguity <= level then
             "Got more than one parse tree.\n\
             \Retry with smaller syntax_ambiguity_level for more information."
           else "";
 
-        val errs = Par_List.map_name "Syntax.disambig" check ts;
-        val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
+        val errs = Par_List.map_name "Syntax.disambig" (check o snd) args;
+        val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs);
         val len = length results;
 
         val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
@@ -782,11 +785,11 @@
             Context_Position.if_visible ctxt warning
               "Fortunately, only one parse tree is type correct.\n\
               \You may still want to disambiguate your grammar or your input."
-          else (); hd results)
+          else (); report_result ctxt (hd results))
         else cat_error (ambig_msg ()) (cat_lines
           (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map show_term (take limit results)))
+            map (show_term o snd) (take limit results)))
       end;
 
 fun standard_parse_term check get_sort map_const map_free ctxt syn root (syms, pos) =
diff -r e10e2cce85c8 -r 1d9710ff7209 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sun Mar 27 15:01:47 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Mar 27 17:55:11 2011 +0200
@@ -13,7 +13,8 @@
   val strip_positions: term -> term
   val strip_positions_ast: Ast.ast -> Ast.ast
   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
-    (string -> bool * string) -> (string -> string option) -> term -> term
+    (string -> bool * string) -> (string -> string option) -> term ->
+    (Position.T * Markup.T) list * term
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
@@ -106,8 +107,10 @@
 
 (* positions *)
 
-fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x)
-  | is_position _ = false;
+fun decode_position (Free (x, _)) = Lexicon.decode_position x
+  | decode_position _ = NONE;
+
+val is_position = is_some o decode_position;
 
 fun strip_positions ((t as Const (c, _)) $ u $ v) =
       if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
@@ -127,35 +130,64 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
+val markup_const = Markup.const;
+fun markup_free x = Markup.name x Markup.free;
+fun markup_var xi = Markup.name (Term.string_of_vname xi) Markup.var;
+fun markup_bound id = Markup.properties [(Markup.idN, id)] Markup.bound;
+
 fun decode_term get_sort map_const map_free tm =
   let
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
-    fun decode (Const ("_constrain", _) $ t $ typ) =
-          if is_position typ then decode t
-          else Type.constraint (decodeT typ) (decode t)
-      | decode (Const ("_constrainAbs", _) $ t $ typ) =
-          if is_position typ then decode t
-          else Type.constraint (decodeT typ --> dummyT) (decode t)
-      | decode (Abs (x, T, t)) = Abs (x, T, decode t)
-      | decode (t $ u) = decode t $ decode u
-      | decode (Const (a, T)) =
+    val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
+    fun report [] _ _ = ()
+      | report ps markup x =
+          let val m = markup x
+          in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end;
+
+    val env0 = ([], [], []);
+
+    fun decode (env as (ps, qs, bs)) (Const ("_constrain", _) $ t $ typ) =
+          (case decode_position typ of
+            SOME p => decode (p :: ps, qs, bs) t
+          | NONE => Type.constraint (decodeT typ) (decode env t))
+      | decode (env as (ps, qs, bs)) (Const ("_constrainAbs", _) $ t $ typ) =
+          (case decode_position typ of
+            SOME q => decode (ps, q :: qs, bs) t
+          | NONE => Type.constraint (decodeT typ --> dummyT) (decode env t))
+      | decode (_, qs, bs) (Abs (x, T, t)) =
+          let
+            val id = serial_string ();
+            val _ = report qs markup_bound id;
+          in Abs (x, T, decode ([], [], (qs, id) :: bs) t) end
+      | decode _ (t $ u) = decode env0 t $ decode env0 u
+      | decode (ps, _, _) (Const (a, T)) =
           (case try Lexicon.unmark_fixed a of
-            SOME x => Free (x, T)
+            SOME x => (report ps markup_free x; Free (x, T))
           | NONE =>
-              let val c =
-                (case try Lexicon.unmark_const a of
-                  SOME c => c
-                | NONE => snd (map_const a))
+              let
+                val c =
+                  (case try Lexicon.unmark_const a of
+                    SOME c => c
+                  | NONE => snd (map_const a));
+                val _ = report ps markup_const c;
               in Const (c, T) end)
-      | decode (Free (a, T)) =
+      | decode (ps, _, _) (Free (a, T)) =
           (case (map_free a, map_const a) of
-            (SOME x, _) => Free (x, T)
-          | (_, (true, c)) => Const (c, T)
-          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
-      | decode (Var (xi, T)) = Var (xi, T)
-      | decode (t as Bound _) = t;
-  in decode tm end;
+            (SOME x, _) => (report ps markup_free x; Free (x, T))
+          | (_, (true, c)) => (report ps markup_const c; Const (c, T))
+          | (_, (false, c)) =>
+              if Long_Name.is_qualified c
+              then (report ps markup_const c; Const (c, T))
+              else (report ps markup_free c; Free (c, T)))
+      | decode (ps, _, _) (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
+      | decode (_, _, bs) (t as Bound i) =
+          (case try (nth bs) i of
+            SOME (qs, id) => (report qs markup_bound id; t)
+          | NONE => t);
+
+    val tm' = decode env0 tm;
+  in (! reports, tm') end;