# 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)