# HG changeset patch # User wenzelm # Date 1185212748 -7200 # Node ID 6234185a2e2e9ac739fa61415ba38a0356bef03e # Parent f2181804fced039b2fc33cb98d2d721a9d3ca624 avoid global reference warned''; diff -r f2181804fced -r 6234185a2e2e 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;