# HG changeset patch
# User kleing
# Date 1312898950 -7200
# Node ID 954e9d6782ea7fa968e50fb1b14721a6084b2794
# Parent  5e14f591515e05a4dada3b5a6f285619c17b0337
removed "extremely ambigous" warning; has been ignored by everyone for years.

diff -r 5e14f591515e -r 954e9d6782ea src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Aug 09 17:33:17 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Aug 09 16:09:10 2011 +0200
@@ -747,7 +747,7 @@
   in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS ctxt warned prods chains Estate i c states =
+fun PROCESSS ctxt prods chains Estate i c states =
   let
     fun all_prods_for nt = prods_for prods chains true c [nt];
 
@@ -773,14 +773,6 @@
                         val tk_prods = all_prods_for nt;
                         val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
                       in (Inttab.update (nt, (min_prec, [])) used, States') end);
-
-                val _ =
-                  if not (! warned) andalso
-                     length new_states + length States > Config.get ctxt branching_level then
-                    (Context_Position.if_visible ctxt warning
-                      "Currently parsed expression could be extremely ambiguous";
-                     warned := true)
-                  else ();
               in
                 processS used' (new_states @ States) (S :: Si, Sii)
               end
@@ -803,7 +795,7 @@
   in processS Inttab.empty states ([], []) end;
 
 
-fun produce ctxt warned prods tags chains stateset i indata prev_token =
+fun produce ctxt prods tags chains stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
@@ -821,10 +813,10 @@
         [] => s
       | c :: cs =>
           let
-            val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
+            val (si, sii) = PROCESSS ctxt prods chains stateset i c s;
             val _ = Array.update (stateset, i, si);
             val _ = Array.update (stateset, i + 1, sii);
-          in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
+          in produce ctxt prods tags chains stateset (i + 1) cs c end));
 
 
 fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
@@ -841,7 +833,7 @@
     val _ = Array.update (Estate, 0, S0);
   in
     get_trees
-      (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
+      (produce ctxt prods tags chains Estate 0 indata Lexicon.eof)
   end;