avoid global reference warned'';
authorwenzelm
Mon, 23 Jul 2007 19:45:48 +0200
changeset 23941 6234185a2e2e
parent 23940 f2181804fced
child 23942 079e99db59d7
avoid global reference warned'';
src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Jul 23 19:45:47 2007 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Jul 23 19:45:48 2007 +0200
@@ -691,7 +691,6 @@
       else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
 
 
-val warned = ref false;                            (*flag for warning message*)
 val branching_level = ref 600;                   (*trigger value for warnings*)
 
 (*get all productions of a NT and NTs chained to it which can
@@ -714,7 +713,7 @@
 in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS prods chains Estate i c states =
+fun PROCESSS warned prods chains Estate i c states =
 let
 fun all_prods_for nt = prods_for prods chains true c [nt];
 
@@ -800,7 +799,7 @@
     error (Pretty.string_of (Pretty.blk (0, [msg, Pretty.fbrk, expected])))
   end;
 
-fun produce prods chains stateset i indata prev_token =
+fun produce warned prods chains stateset i indata prev_token =
                                       (*prev_token is used for error messages*)
   (case Array.sub (stateset, i) of
     [] => let fun some_prods_for tk nt = prods_for prods chains false tk [nt];
@@ -855,10 +854,10 @@
     (case indata of
        [] => Array.sub (stateset, i)
      | c :: cs =>
-       let val (si, sii) = PROCESSS prods chains stateset i c s;
+       let val (si, sii) = PROCESSS warned prods chains stateset i c s;
        in Array.update (stateset, i, si);
           Array.update (stateset, i + 1, sii);
-          produce prods chains stateset (i + 1) cs c
+          produce warned prods chains stateset (i + 1) cs c
        end));
 
 
@@ -877,8 +876,7 @@
     val Estate = Array.array (s, []);
   in
     Array.update (Estate, 0, S0);
-    warned := false;
-    get_trees (produce prods chains Estate 0 indata EndToken)
+    get_trees (produce (ref false) prods chains Estate 0 indata EndToken)
   end;