# HG changeset patch # User wenzelm # Date 1283546176 -7200 # Node ID ee117c5b3b758480b44e1b3ebda2304c0061063d # Parent f45d332a90e306e11d9bc2cdcc1d943fb1f3db5f configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit; diff -r f45d332a90e3 -r ee117c5b3b75 NEWS --- a/NEWS Fri Sep 03 21:13:53 2010 +0200 +++ b/NEWS Fri Sep 03 22:36:16 2010 +0200 @@ -30,18 +30,20 @@ ML (Config.T) Isar (attribute) + show_question_marks show_question_marks + show_consts show_consts + + Syntax.ambiguity_level syntax_ambiguity_level + + Goal_Display.goals_limit goals_limit + Goal_Display.show_main_goal show_main_goal + Thy_Output.display thy_output_display Thy_Output.quotes thy_output_quotes Thy_Output.indent thy_output_indent Thy_Output.source thy_output_source Thy_Output.break thy_output_break - show_question_marks show_question_marks - show_consts show_consts - - Goal_Display.goals_limit goals_limit - Goal_Display.show_main_goal show_main_goal - Note that corresponding "..._default" references in ML may be only changed globally at the ROOT session setup, but *not* within a theory. diff -r f45d332a90e3 -r ee117c5b3b75 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri Sep 03 21:13:53 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri Sep 03 22:36:16 2010 +0200 @@ -189,7 +189,9 @@ fun simple_smart_string_of_cterm ctxt0 ct = let - val ctxt = Config.put show_all_types true ctxt0; + val ctxt = ctxt0 + |> Config.put show_all_types true + |> Config.put Syntax.ambiguity_enabled true; val {t,T,...} = rep_cterm ct (* Hack to avoid parse errors with Trueprop *) val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t) @@ -198,15 +200,15 @@ quote ( Print_Mode.setmp [] ( setmp_CRITICAL show_brackets false ( - setmp_CRITICAL Syntax.ambiguity_is_error false ( - setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))) + setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))) ct) end exception SMART_STRING -fun smart_string_of_cterm ctxt ct = +fun smart_string_of_cterm ctxt0 ct = let + val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false; val {t,T,...} = rep_cterm ct (* Hack to avoid parse errors with Trueprop *) val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t) @@ -232,9 +234,9 @@ | SMART_STRING => error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct)) in - Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0 + Print_Mode.setmp [] F 0 end - handle ERROR mesg => simple_smart_string_of_cterm ctxt ct + handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of diff -r f45d332a90e3 -r ee117c5b3b75 src/HOL/Lambda/Commutation.thy --- a/src/HOL/Lambda/Commutation.thy Fri Sep 03 21:13:53 2010 +0200 +++ b/src/HOL/Lambda/Commutation.thy Fri Sep 03 22:36:16 2010 +0200 @@ -7,6 +7,9 @@ theory Commutation imports Main begin +declare [[syntax_ambiguity_level = 100]] + + subsection {* Basic definitions *} definition diff -r f45d332a90e3 -r ee117c5b3b75 src/HOL/Lambda/Lambda.thy --- a/src/HOL/Lambda/Lambda.thy Fri Sep 03 21:13:53 2010 +0200 +++ b/src/HOL/Lambda/Lambda.thy Fri Sep 03 22:36:16 2010 +0200 @@ -7,6 +7,8 @@ theory Lambda imports Main begin +declare [[syntax_ambiguity_level = 100]] + subsection {* Lambda-terms in de Bruijn notation and substitution *} diff -r f45d332a90e3 -r ee117c5b3b75 src/HOL/Lambda/ListOrder.thy --- a/src/HOL/Lambda/ListOrder.thy Fri Sep 03 21:13:53 2010 +0200 +++ b/src/HOL/Lambda/ListOrder.thy Fri Sep 03 22:36:16 2010 +0200 @@ -7,6 +7,9 @@ theory ListOrder imports Main begin +declare [[syntax_ambiguity_level = 100]] + + text {* Lifting an order to lists of elements, relating exactly one element. diff -r f45d332a90e3 -r ee117c5b3b75 src/HOL/Lambda/ROOT.ML --- a/src/HOL/Lambda/ROOT.ML Fri Sep 03 21:13:53 2010 +0200 +++ b/src/HOL/Lambda/ROOT.ML Fri Sep 03 22:36:16 2010 +0200 @@ -1,4 +1,2 @@ -Syntax.ambiguity_level := 100; - no_document use_thys ["Code_Integer"]; use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; diff -r f45d332a90e3 -r ee117c5b3b75 src/HOL/MicroJava/J/JListExample.thy --- a/src/HOL/MicroJava/J/JListExample.thy Fri Sep 03 21:13:53 2010 +0200 +++ b/src/HOL/MicroJava/J/JListExample.thy Fri Sep 03 22:36:16 2010 +0200 @@ -8,7 +8,7 @@ imports Eval begin -ML {* Syntax.ambiguity_level := 100000 *} +declare [[syntax_ambiguity_level = 100000]] consts list_name :: cname diff -r f45d332a90e3 -r ee117c5b3b75 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Sep 03 21:13:53 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Sep 03 22:36:16 2010 +0200 @@ -393,6 +393,7 @@ val _ = Context.>> (Context.map_theory (register_config Syntax.show_question_marks_value #> + register_config Syntax.ambiguity_level_value #> register_config Goal_Display.goals_limit_value #> register_config Goal_Display.show_main_goal_value #> register_config Goal_Display.show_consts_value #> diff -r f45d332a90e3 -r ee117c5b3b75 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Sep 03 21:13:53 2010 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Sep 03 22:36:16 2010 +0200 @@ -36,9 +36,10 @@ val print_syntax: syntax -> unit val guess_infix: syntax -> string -> mixfix option val read_token: string -> Symbol_Pos.T list * Position.T - val ambiguity_is_error: bool Unsynchronized.ref - val ambiguity_level: int Unsynchronized.ref - val ambiguity_limit: int Unsynchronized.ref + val ambiguity_enabled: bool Config.T + val ambiguity_level_value: Config.value Config.T + val ambiguity_level: int Config.T + val ambiguity_limit: int Config.T val standard_parse_term: Pretty.pp -> (term -> string option) -> (((string * int) * sort) list -> string * int -> Term.sort) -> (string -> bool * string) -> (string -> string option) -> Proof.context -> @@ -472,9 +473,14 @@ (* read_ast *) -val ambiguity_is_error = Unsynchronized.ref false; -val ambiguity_level = Unsynchronized.ref 1; -val ambiguity_limit = Unsynchronized.ref 10; +val ambiguity_enabled = + Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true)); + +val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1); +val ambiguity_level = Config.int ambiguity_level_value; + +val ambiguity_limit = + Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10)); fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos; @@ -488,12 +494,12 @@ val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks); val len = length pts; - val limit = ! ambiguity_limit; + val limit = Config.get ctxt ambiguity_limit; fun show_pt pt = Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt]))); in - if len <= ! ambiguity_level then () - else if ! ambiguity_is_error then error (ambiguity_msg pos) + if len <= Config.get ctxt ambiguity_level then () + else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos) else (Context_Position.if_visible ctxt warning (cat_lines (("Ambiguous input" ^ Position.str_of pos ^ @@ -522,14 +528,14 @@ fun disambig _ _ _ [t] = t | disambig ctxt pp check ts = let - val level = ! ambiguity_level; - val limit = ! ambiguity_limit; + val level = Config.get ctxt ambiguity_level; + val limit = Config.get ctxt ambiguity_limit; val ambiguity = length ts; fun ambig_msg () = if ambiguity > 1 andalso ambiguity <= level then "Got more than one parse tree.\n\ - \Retry with smaller Syntax.ambiguity_level for more information." + \Retry with smaller syntax_ambiguity_level for more information." else ""; val errs = Par_List.map check ts;