configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
authorwenzelm
Fri Sep 03 22:36:16 2010 +0200 (2010-09-03)
changeset 39126ee117c5b3b75
parent 39125 f45d332a90e3
child 39127 e7ecbe86d22e
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
NEWS
src/HOL/Import/proof_kernel.ML
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ROOT.ML
src/HOL/MicroJava/J/JListExample.thy
src/Pure/Isar/attrib.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/NEWS	Fri Sep 03 21:13:53 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 03 22:36:16 2010 +0200
     1.3 @@ -30,18 +30,20 @@
     1.4  
     1.5    ML (Config.T)                 Isar (attribute)
     1.6  
     1.7 +  show_question_marks           show_question_marks
     1.8 +  show_consts                   show_consts
     1.9 +
    1.10 +  Syntax.ambiguity_level        syntax_ambiguity_level
    1.11 +
    1.12 +  Goal_Display.goals_limit      goals_limit
    1.13 +  Goal_Display.show_main_goal   show_main_goal
    1.14 +
    1.15    Thy_Output.display            thy_output_display
    1.16    Thy_Output.quotes             thy_output_quotes
    1.17    Thy_Output.indent             thy_output_indent
    1.18    Thy_Output.source             thy_output_source
    1.19    Thy_Output.break              thy_output_break
    1.20  
    1.21 -  show_question_marks           show_question_marks
    1.22 -  show_consts                   show_consts
    1.23 -
    1.24 -  Goal_Display.goals_limit      goals_limit
    1.25 -  Goal_Display.show_main_goal   show_main_goal
    1.26 -
    1.27  Note that corresponding "..._default" references in ML may be only
    1.28  changed globally at the ROOT session setup, but *not* within a theory.
    1.29  
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Sep 03 21:13:53 2010 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 03 22:36:16 2010 +0200
     2.3 @@ -189,7 +189,9 @@
     2.4  
     2.5  fun simple_smart_string_of_cterm ctxt0 ct =
     2.6      let
     2.7 -        val ctxt = Config.put show_all_types true ctxt0;
     2.8 +        val ctxt = ctxt0
     2.9 +          |> Config.put show_all_types true
    2.10 +          |> Config.put Syntax.ambiguity_enabled true;
    2.11          val {t,T,...} = rep_cterm ct
    2.12          (* Hack to avoid parse errors with Trueprop *)
    2.13          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    2.14 @@ -198,15 +200,15 @@
    2.15          quote (
    2.16          Print_Mode.setmp [] (
    2.17          setmp_CRITICAL show_brackets false (
    2.18 -        setmp_CRITICAL Syntax.ambiguity_is_error false (
    2.19 -        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))))
    2.20 +        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
    2.21          ct)
    2.22      end
    2.23  
    2.24  exception SMART_STRING
    2.25  
    2.26 -fun smart_string_of_cterm ctxt ct =
    2.27 +fun smart_string_of_cterm ctxt0 ct =
    2.28      let
    2.29 +        val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false;
    2.30          val {t,T,...} = rep_cterm ct
    2.31          (* Hack to avoid parse errors with Trueprop *)
    2.32          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    2.33 @@ -232,9 +234,9 @@
    2.34                | SMART_STRING =>
    2.35                    error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
    2.36      in
    2.37 -      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    2.38 +      Print_Mode.setmp [] F 0
    2.39      end
    2.40 -    handle ERROR mesg => simple_smart_string_of_cterm ctxt ct
    2.41 +    handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct
    2.42  
    2.43  fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
    2.44  
     3.1 --- a/src/HOL/Lambda/Commutation.thy	Fri Sep 03 21:13:53 2010 +0200
     3.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Sep 03 22:36:16 2010 +0200
     3.3 @@ -7,6 +7,9 @@
     3.4  
     3.5  theory Commutation imports Main begin
     3.6  
     3.7 +declare [[syntax_ambiguity_level = 100]]
     3.8 +
     3.9 +
    3.10  subsection {* Basic definitions *}
    3.11  
    3.12  definition
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Fri Sep 03 21:13:53 2010 +0200
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Sep 03 22:36:16 2010 +0200
     4.3 @@ -7,6 +7,8 @@
     4.4  
     4.5  theory Lambda imports Main begin
     4.6  
     4.7 +declare [[syntax_ambiguity_level = 100]]
     4.8 +
     4.9  
    4.10  subsection {* Lambda-terms in de Bruijn notation and substitution *}
    4.11  
     5.1 --- a/src/HOL/Lambda/ListOrder.thy	Fri Sep 03 21:13:53 2010 +0200
     5.2 +++ b/src/HOL/Lambda/ListOrder.thy	Fri Sep 03 22:36:16 2010 +0200
     5.3 @@ -7,6 +7,9 @@
     5.4  
     5.5  theory ListOrder imports Main begin
     5.6  
     5.7 +declare [[syntax_ambiguity_level = 100]]
     5.8 +
     5.9 +
    5.10  text {*
    5.11    Lifting an order to lists of elements, relating exactly one
    5.12    element.
     6.1 --- a/src/HOL/Lambda/ROOT.ML	Fri Sep 03 21:13:53 2010 +0200
     6.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Sep 03 22:36:16 2010 +0200
     6.3 @@ -1,4 +1,2 @@
     6.4 -Syntax.ambiguity_level := 100;
     6.5 -
     6.6  no_document use_thys ["Code_Integer"];
     6.7  use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];
     7.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Fri Sep 03 21:13:53 2010 +0200
     7.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Sep 03 22:36:16 2010 +0200
     7.3 @@ -8,7 +8,7 @@
     7.4  imports Eval
     7.5  begin
     7.6  
     7.7 -ML {* Syntax.ambiguity_level := 100000 *}
     7.8 +declare [[syntax_ambiguity_level = 100000]]
     7.9  
    7.10  consts
    7.11    list_name :: cname
     8.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 21:13:53 2010 +0200
     8.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 22:36:16 2010 +0200
     8.3 @@ -393,6 +393,7 @@
     8.4  
     8.5  val _ = Context.>> (Context.map_theory
     8.6   (register_config Syntax.show_question_marks_value #>
     8.7 +  register_config Syntax.ambiguity_level_value #>
     8.8    register_config Goal_Display.goals_limit_value #>
     8.9    register_config Goal_Display.show_main_goal_value #>
    8.10    register_config Goal_Display.show_consts_value #>
     9.1 --- a/src/Pure/Syntax/syntax.ML	Fri Sep 03 21:13:53 2010 +0200
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Sep 03 22:36:16 2010 +0200
     9.3 @@ -36,9 +36,10 @@
     9.4    val print_syntax: syntax -> unit
     9.5    val guess_infix: syntax -> string -> mixfix option
     9.6    val read_token: string -> Symbol_Pos.T list * Position.T
     9.7 -  val ambiguity_is_error: bool Unsynchronized.ref
     9.8 -  val ambiguity_level: int Unsynchronized.ref
     9.9 -  val ambiguity_limit: int Unsynchronized.ref
    9.10 +  val ambiguity_enabled: bool Config.T
    9.11 +  val ambiguity_level_value: Config.value Config.T
    9.12 +  val ambiguity_level: int Config.T
    9.13 +  val ambiguity_limit: int Config.T
    9.14    val standard_parse_term: Pretty.pp -> (term -> string option) ->
    9.15      (((string * int) * sort) list -> string * int -> Term.sort) ->
    9.16      (string -> bool * string) -> (string -> string option) -> Proof.context ->
    9.17 @@ -472,9 +473,14 @@
    9.18  
    9.19  (* read_ast *)
    9.20  
    9.21 -val ambiguity_is_error = Unsynchronized.ref false;
    9.22 -val ambiguity_level = Unsynchronized.ref 1;
    9.23 -val ambiguity_limit = Unsynchronized.ref 10;
    9.24 +val ambiguity_enabled =
    9.25 +  Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
    9.26 +
    9.27 +val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
    9.28 +val ambiguity_level = Config.int ambiguity_level_value;
    9.29 +
    9.30 +val ambiguity_limit =
    9.31 +  Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
    9.32  
    9.33  fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
    9.34  
    9.35 @@ -488,12 +494,12 @@
    9.36      val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
    9.37      val len = length pts;
    9.38  
    9.39 -    val limit = ! ambiguity_limit;
    9.40 +    val limit = Config.get ctxt ambiguity_limit;
    9.41      fun show_pt pt =
    9.42        Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
    9.43    in
    9.44 -    if len <= ! ambiguity_level then ()
    9.45 -    else if ! ambiguity_is_error then error (ambiguity_msg pos)
    9.46 +    if len <= Config.get ctxt ambiguity_level then ()
    9.47 +    else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
    9.48      else
    9.49        (Context_Position.if_visible ctxt warning (cat_lines
    9.50          (("Ambiguous input" ^ Position.str_of pos ^
    9.51 @@ -522,14 +528,14 @@
    9.52  fun disambig _ _ _ [t] = t
    9.53    | disambig ctxt pp check ts =
    9.54        let
    9.55 -        val level = ! ambiguity_level;
    9.56 -        val limit = ! ambiguity_limit;
    9.57 +        val level = Config.get ctxt ambiguity_level;
    9.58 +        val limit = Config.get ctxt ambiguity_limit;
    9.59  
    9.60          val ambiguity = length ts;
    9.61          fun ambig_msg () =
    9.62            if ambiguity > 1 andalso ambiguity <= level then
    9.63              "Got more than one parse tree.\n\
    9.64 -            \Retry with smaller Syntax.ambiguity_level for more information."
    9.65 +            \Retry with smaller syntax_ambiguity_level for more information."
    9.66            else "";
    9.67  
    9.68          val errs = Par_List.map check ts;