# HG changeset patch
# User wenzelm
# Date 1314528811 -7200
# Node ID 96ba83710946fbfb399c592b53afe3da2755cf4f
# Parent  01b2732cf4ad1072be0ae3e86c2f991870ac9802
tuned positions of ambiguity messages -- less intrusive in IDE view;

diff -r 01b2732cf4ad -r 96ba83710946 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Aug 28 08:43:25 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Aug 28 12:53:31 2011 +0200
@@ -294,7 +294,7 @@
       else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
       else if warnings then
         (Context_Position.if_visible ctxt warning (cat_lines
-          (("Ambiguous input" ^ Position.str_of pos ^
+          (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
             "\nproduces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
@@ -386,8 +386,9 @@
           else if len = 1 then
             (if ambiguity > level andalso warnings then
               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."
+                ("Fortunately, only one parse tree is type correct" ^
+                Position.str_of (Position.reset_range pos) ^
+                ",\nbut you may still want to disambiguate your grammar or your input.")
             else (); report_result ctxt pos results')
           else
             report_result ctxt pos