--- a/src/Pure/Syntax/parser.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Sep 29 11:49:22 2009 +0200
@@ -17,7 +17,7 @@
Tip of Lexicon.token
val parse: gram -> string -> Lexicon.token list -> parsetree list
val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
- val branching_level: int ref
+ val branching_level: int Unsynchronized.ref
end;
structure Parser: PARSER =
@@ -690,7 +690,7 @@
else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
-val branching_level = ref 600; (*trigger value for warnings*)
+val branching_level = Unsynchronized.ref 600; (*trigger value for warnings*)
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
@@ -821,7 +821,7 @@
val Estate = Array.array (s, []);
in
Array.update (Estate, 0, S0);
- get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
+ get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
end;