# HG changeset patch
# User wenzelm
# Date 1292963496 -3600
# Node ID 55286df6a423b32be853a135e7c1068e5873fb7f
# Parent  390c539042205624058979b14de296fabba078dd
configuration option "syntax_branching_level";

diff -r 390c53904220 -r 55286df6a423 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Dec 21 21:21:21 2010 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Dec 21 21:31:36 2010 +0100
@@ -17,7 +17,7 @@
     Tip of Lexicon.token
   val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
   val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
-  val branching_level: int Unsynchronized.ref
+  val branching_level: int Config.T
 end;
 
 structure Parser: PARSER =
@@ -715,7 +715,8 @@
       else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
 
 
-val branching_level = Unsynchronized.ref 600;   (*trigger value for warnings*)
+(*trigger value for warnings*)
+val branching_level = Config.int (Config.declare "syntax_branching_level" (fn _ => Config.Int 600));
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
@@ -771,7 +772,7 @@
 
                 val dummy =
                   if not (! warned) andalso
-                     length (new_states @ States) > ! branching_level then
+                     length (new_states @ States) > Config.get ctxt branching_level then
                     (Context_Position.if_visible ctxt warning
                       "Currently parsed expression could be extremely ambiguous";
                      warned := true)