src/Pure/Syntax/parser.ML

   datatype parsetree =
     Node of string * parsetree list |
     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 =
 struct
 

         (B, j, tss @ t, sa, id, i) ::
           movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts
       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*)
 fun prods_for prods chains include_none tk nts =
 let

     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal eof], "", 0)];
     val s = length indata + 1;
     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;
 
 
 fun parse (Gram {tags, prods, chains, ...}) start toks =
   let