# HG changeset patch
# User wenzelm
# Date 1120221725 -7200
# Node ID 507438b27f66c428c345482b0ab8efd8986e029f
# Parent  76613dff2c9a8e4a37066d3a95021321f1a3c031
use tracing for potentially voluminous ambiguity output;

diff -r 76613dff2c9a -r 507438b27f66 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jul 01 14:42:04 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jul 01 14:42:05 2005 +0200
@@ -369,8 +369,9 @@
   in
     conditional (length pts > ! ambiguity_level) (fn () =>
       if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
-      else warning (cat_lines ("Ambiguous input " ^ quote str ::
-        "produces the following parse trees:" :: map show_pt pts)));
+      else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
+          "produces " ^ string_of_int (length pts) ^ " parse trees (see trace).");
+         List.app (tracing o show_pt) pts));
     SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts
   end;