Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use tracing for potentially voluminous ambiguity output;
authorwenzelm
Fri, 01 Jul 2005 14:42:05 +0200
changeset 16661 507438b27f66
parent 16660 76613dff2c9a
child 16662 0836569a8ffc
use tracing for potentially voluminous ambiguity output;
src/Pure/Syntax/syntax.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle