# HG changeset patch
# User wenzelm
# Date 1394204445 -3600
# Node ID 06cb126f30ba7a5059e703f1a7c230b349953071
# Parent  56645c447ee989e0a2f1b82e62fb4890fb1b0bcd
tuned message: reveal ambiguity where Syntax_Phases.decode_term fails and thus reduces proper_results beforehand, e.g. term "f(x := y)" in ~~/src/HOL/Hoare/Hoare_Logic.thy;

diff -r 56645c447ee9 -r 06cb126f30ba src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 15:16:08 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 16:00:45 2014 +0100
@@ -337,7 +337,7 @@
       else
         [cat_lines
           (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
-            "\nproduces " ^ string_of_int len ^ " parse trees" ^
+            " produces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
               (take limit pts))];
@@ -417,12 +417,11 @@
             report_result ctxt pos []
               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
           else if checked_len = 1 then
-            (if parsed_len > 1 andalso ambiguity_warning then
+            (if not (null ambig_msgs) andalso ambiguity_warning then
               Context_Position.if_visible ctxt warning
                 (cat_lines (ambig_msgs @
-                  ["Fortunately, only one parse tree is type correct" ^
-                  Position.here (Position.reset_range pos) ^
-                  ",\nbut you may still want to disambiguate your grammar or your input."]))
+                  ["Fortunately, only one parse tree is well-formed and type-correct,\n\
+                   \but you may still want to disambiguate your grammar or your input."]))
              else (); report_result ctxt pos [] results')
           else
             report_result ctxt pos []