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;
authorwenzelm
Fri Mar 07 16:00:45 2014 +0100 (2014-03-07)
changeset 5597906cb126f30ba
parent 55978 56645c447ee9
child 55980 36fd4981c119
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;
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 15:16:08 2014 +0100
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 16:00:45 2014 +0100
     1.3 @@ -337,7 +337,7 @@
     1.4        else
     1.5          [cat_lines
     1.6            (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
     1.7 -            "\nproduces " ^ string_of_int len ^ " parse trees" ^
     1.8 +            " produces " ^ string_of_int len ^ " parse trees" ^
     1.9              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    1.10              map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
    1.11                (take limit pts))];
    1.12 @@ -417,12 +417,11 @@
    1.13              report_result ctxt pos []
    1.14                [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
    1.15            else if checked_len = 1 then
    1.16 -            (if parsed_len > 1 andalso ambiguity_warning then
    1.17 +            (if not (null ambig_msgs) andalso ambiguity_warning then
    1.18                Context_Position.if_visible ctxt warning
    1.19                  (cat_lines (ambig_msgs @
    1.20 -                  ["Fortunately, only one parse tree is type correct" ^
    1.21 -                  Position.here (Position.reset_range pos) ^
    1.22 -                  ",\nbut you may still want to disambiguate your grammar or your input."]))
    1.23 +                  ["Fortunately, only one parse tree is well-formed and type-correct,\n\
    1.24 +                   \but you may still want to disambiguate your grammar or your input."]))
    1.25               else (); report_result ctxt pos [] results')
    1.26            else
    1.27              report_result ctxt pos []