1.1 --- a/src/Pure/Syntax/parser.ML	Tue Aug 09 17:33:17 2011 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Tue Aug 09 16:09:10 2011 +0200
     1.3 @@ -747,7 +747,7 @@
     1.4    in get_prods (connected_with chains nts nts) [] end;
     1.5  
     1.6  
     1.7 -fun PROCESSS ctxt warned prods chains Estate i c states =
     1.8 +fun PROCESSS ctxt prods chains Estate i c states =
     1.9    let
    1.10      fun all_prods_for nt = prods_for prods chains true c [nt];
    1.11  
    1.12 @@ -773,14 +773,6 @@
    1.13                          val tk_prods = all_prods_for nt;
    1.14                          val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
    1.15                        in (Inttab.update (nt, (min_prec, [])) used, States') end);
    1.16 -
    1.17 -                val _ =
    1.18 -                  if not (! warned) andalso
    1.19 -                     length new_states + length States > Config.get ctxt branching_level then
    1.20 -                    (Context_Position.if_visible ctxt warning
    1.21 -                      "Currently parsed expression could be extremely ambiguous";
    1.22 -                     warned := true)
    1.23 -                  else ();
    1.24                in
    1.25                  processS used' (new_states @ States) (S :: Si, Sii)
    1.26                end
    1.27 @@ -803,7 +795,7 @@
    1.28    in processS Inttab.empty states ([], []) end;
    1.29  
    1.30  
    1.31 -fun produce ctxt warned prods tags chains stateset i indata prev_token =
    1.32 +fun produce ctxt prods tags chains stateset i indata prev_token =
    1.33    (case Array.sub (stateset, i) of
    1.34      [] =>
    1.35        let
    1.36 @@ -821,10 +813,10 @@
    1.37          [] => s
    1.38        | c :: cs =>
    1.39            let
    1.40 -            val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
    1.41 +            val (si, sii) = PROCESSS ctxt prods chains stateset i c s;
    1.42              val _ = Array.update (stateset, i, si);
    1.43              val _ = Array.update (stateset, i + 1, sii);
    1.44 -          in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
    1.45 +          in produce ctxt prods tags chains stateset (i + 1) cs c end));
    1.46  
    1.47  
    1.48  fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
    1.49 @@ -841,7 +833,7 @@
    1.50      val _ = Array.update (Estate, 0, S0);
    1.51    in
    1.52      get_trees
    1.53 -      (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
    1.54 +      (produce ctxt prods tags chains Estate 0 indata Lexicon.eof)
    1.55    end;
    1.56  
    1.57