--- 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