# HG changeset patch # User wenzelm # Date 1329489746 -3600 # Node ID 4f9f61f9b535ab670149d244b68bc608fa22ec72 # Parent fbb3c68a8d3c0208f6c32218be4d64c17b5633e4 simplified configuration options for syntax ambiguity; diff -r fbb3c68a8d3c -r 4f9f61f9b535 NEWS --- a/NEWS Fri Feb 17 11:24:39 2012 +0100 +++ b/NEWS Fri Feb 17 15:42:26 2012 +0100 @@ -37,8 +37,8 @@ position information via constraints). * Simplified configuration options for syntax ambiguity: see -"syntax_ambiguity" and "syntax_ambiguity_limit" in isar-ref manual. -Minor INCOMPATIBILITY. +"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref +manual. Minor INCOMPATIBILITY. *** Pure *** diff -r fbb3c68a8d3c -r 4f9f61f9b535 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Feb 17 11:24:39 2012 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Feb 17 15:42:26 2012 +0100 @@ -980,7 +980,7 @@ text {* \begin{tabular}{rcll} - @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\ + @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\ @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\ \end{tabular} @@ -1000,9 +1000,8 @@ \begin{description} - \item @{attribute syntax_ambiguity} determines reaction on multiple - results of parsing; this string option can be set to @{text - "ignore"}, @{text "warning"}, or @{text "error"}. + \item @{attribute syntax_ambiguity_warning} controls output of + explicit warning messages about syntax ambiguity. \item @{attribute syntax_ambiguity_limit} determines the number of resulting parse trees that are shown as part of the printed message diff -r fbb3c68a8d3c -r 4f9f61f9b535 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Feb 17 11:24:39 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Feb 17 15:42:26 2012 +0100 @@ -1154,7 +1154,7 @@ % \begin{isamarkuptext}% \begin{tabular}{rcll} - \indexdef{}{attribute}{syntax\_ambiguity}\hypertarget{attribute.syntax-ambiguity}{\hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}}} & : & \isa{attribute} & default \isa{warning} \\ + \indexdef{}{attribute}{syntax\_ambiguity\_warning}\hypertarget{attribute.syntax-ambiguity-warning}{\hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}}} & : & \isa{attribute} & default \isa{true} \\ \indexdef{}{attribute}{syntax\_ambiguity\_limit}\hypertarget{attribute.syntax-ambiguity-limit}{\hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\ \end{tabular} @@ -1174,8 +1174,8 @@ \begin{description} - \item \hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}} determines reaction on multiple - results of parsing; this string option can be set to \isa{{\isaliteral{22}{\isachardoublequote}}ignore{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}warning{\isaliteral{22}{\isachardoublequote}}}, or \isa{{\isaliteral{22}{\isachardoublequote}}error{\isaliteral{22}{\isachardoublequote}}}. + \item \hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}} controls output of + explicit warning messages about syntax ambiguity. \item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of resulting parse trees that are shown as part of the printed message diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/HOL/MicroJava/J/JListExample.thy --- a/src/HOL/MicroJava/J/JListExample.thy Fri Feb 17 11:24:39 2012 +0100 +++ b/src/HOL/MicroJava/J/JListExample.thy Fri Feb 17 15:42:26 2012 +0100 @@ -8,7 +8,7 @@ imports Eval begin -declare [[syntax_ambiguity = ignore]] +declare [[syntax_ambiguity_warning = false]] consts list_nam :: cnam diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/HOL/Proofs/Lambda/Commutation.thy --- a/src/HOL/Proofs/Lambda/Commutation.thy Fri Feb 17 11:24:39 2012 +0100 +++ b/src/HOL/Proofs/Lambda/Commutation.thy Fri Feb 17 15:42:26 2012 +0100 @@ -7,7 +7,7 @@ theory Commutation imports Main begin -declare [[syntax_ambiguity = ignore]] +declare [[syntax_ambiguity_warning = false]] subsection {* Basic definitions *} diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/HOL/Proofs/Lambda/Lambda.thy --- a/src/HOL/Proofs/Lambda/Lambda.thy Fri Feb 17 11:24:39 2012 +0100 +++ b/src/HOL/Proofs/Lambda/Lambda.thy Fri Feb 17 15:42:26 2012 +0100 @@ -7,7 +7,7 @@ theory Lambda imports Main begin -declare [[syntax_ambiguity = ignore]] +declare [[syntax_ambiguity_warning = false]] subsection {* Lambda-terms in de Bruijn notation and substitution *} diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/HOL/Proofs/Lambda/ListOrder.thy --- a/src/HOL/Proofs/Lambda/ListOrder.thy Fri Feb 17 11:24:39 2012 +0100 +++ b/src/HOL/Proofs/Lambda/ListOrder.thy Fri Feb 17 15:42:26 2012 +0100 @@ -7,7 +7,7 @@ theory ListOrder imports Main begin -declare [[syntax_ambiguity = ignore]] +declare [[syntax_ambiguity_warning = false]] text {* diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Feb 17 11:24:39 2012 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Feb 17 15:42:26 2012 +0100 @@ -503,7 +503,7 @@ register_config Printer.show_types_raw #> register_config Printer.show_structs_raw #> register_config Printer.show_question_marks_raw #> - register_config Syntax.ambiguity_raw #> + register_config Syntax.ambiguity_warning_raw #> register_config Syntax.ambiguity_limit_raw #> register_config Syntax_Trans.eta_contract_raw #> register_config Name_Space.names_long_raw #> diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Feb 17 11:24:39 2012 +0100 +++ b/src/Pure/Syntax/syntax.ML Fri Feb 17 15:42:26 2012 +0100 @@ -10,8 +10,8 @@ type operations val install_operations: operations -> unit val root: string Config.T - val ambiguity_raw: Config.raw - val ambiguity: string Config.T + val ambiguity_warning_raw: Config.raw + val ambiguity_warning: bool Config.T val ambiguity_limit_raw: Config.raw val ambiguity_limit: int Config.T val read_token: string -> Symbol_Pos.T list * Position.T @@ -155,8 +155,8 @@ val root = Config.string (Config.declare "syntax_root" (K (Config.String "any"))); -val ambiguity_raw = Config.declare "syntax_ambiguity" (fn _ => Config.String "warning"); -val ambiguity = Config.string ambiguity_raw; +val ambiguity_warning_raw = Config.declare "syntax_ambiguity_warning" (fn _ => Config.Bool true); +val ambiguity_warning = Config.bool ambiguity_warning_raw; val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10); val ambiguity_limit = Config.int ambiguity_limit_raw; diff -r fbb3c68a8d3c -r 4f9f61f9b535 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Feb 17 11:24:39 2012 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Feb 17 15:42:26 2012 +0100 @@ -262,11 +262,14 @@ fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results; fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results; -fun report_result ctxt pos results = +fun report_result ctxt pos ambig_msgs results = (case (proper_results results, failed_results results) of ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn) | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x) - | _ => error ("Parse error: ambiguous syntax" ^ Position.str_of pos)); + | _ => + if null ambig_msgs then + error ("Parse error: ambiguous syntax" ^ Position.str_of pos) + else error (cat_lines ambig_msgs)); (* parse raw asts *) @@ -286,36 +289,28 @@ (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks)); val len = length pts; - val ambiguity = Config.get ctxt Syntax.ambiguity; - val _ = - member (op =) ["ignore", "warning", "error"] ambiguity orelse - error ("Bad value for syntax_ambiguity: " ^ quote ambiguity); - val limit = Config.get ctxt Syntax.ambiguity_limit; - - val _ = - if len <= 1 orelse ambiguity = "ignore" then () + val ambig_msgs = + if len <= 1 then [] else - (if ambiguity = "error" then error else Context_Position.if_visible ctxt warning) - (cat_lines - (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^ - "\nproduces " ^ string_of_int len ^ " parse trees" ^ - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: - map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))); - in - map (parsetree_to_ast ctxt raw ast_tr) pts - end; + [cat_lines + (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^ + "\nproduces " ^ string_of_int len ^ " parse trees" ^ + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: + map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))]; + + in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end; fun parse_tree ctxt root input = let val syn = Proof_Context.syn_of ctxt; val tr = Syntax.parse_translation syn; val parse_rules = Syntax.parse_rules syn; - in - parse_asts ctxt false root input - |> (map o apsnd o Exn.maps_result) - (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) - end; + val (ambig_msgs, asts) = parse_asts ctxt false root input; + val results = + (map o apsnd o Exn.maps_result) + (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts; + in (ambig_msgs, results) end; (* parse logical entities *) @@ -329,7 +324,7 @@ Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort (fn (syms, pos) => parse_tree ctxt "sort" (syms, pos) - |> report_result ctxt pos + |> uncurry (report_result ctxt pos) |> decode_sort |> Type.minimize_sort (Proof_Context.tsig_of ctxt) handle ERROR msg => parse_failed ctxt pos msg "sort"); @@ -338,7 +333,7 @@ Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ (fn (syms, pos) => parse_tree ctxt "type" (syms, pos) - |> report_result ctxt pos + |> uncurry (report_result ctxt pos) |> decode_typ handle ERROR msg => parse_failed ctxt pos msg "type"); @@ -353,18 +348,12 @@ Syntax.parse_token ctxt decode markup (fn (syms, pos) => let - val results = parse_tree ctxt root (syms, pos) |> map (decode_term ctxt); + val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt); val parsed_len = length (proper_results results); - val ambiguity = Config.get ctxt Syntax.ambiguity; + val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning; val limit = Config.get ctxt Syntax.ambiguity_limit; - val ambig_msg = - if parsed_len > 1 andalso ambiguity = "ignore" then - ["Got more than one parse tree.\n\ - \Retry with syntax_ambiguity = \"warning\" for more information."] - else []; - (*brute-force disambiguation via type-inference*) fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t) handle exn as ERROR _ => Exn.Exn exn; @@ -383,19 +372,20 @@ val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt); in if checked_len = 0 then - report_result ctxt pos - [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))] + report_result ctxt pos [] + [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))] else if checked_len = 1 then - (if parsed_len > 1 andalso ambiguity <> "ignore" then + (if parsed_len > 1 andalso ambiguity_warning then Context_Position.if_visible ctxt warning - ("Fortunately, only one parse tree is type correct" ^ - Position.str_of (Position.reset_range pos) ^ - ",\nbut you may still want to disambiguate your grammar or your input.") - else (); report_result ctxt pos results') + (cat_lines (ambig_msgs @ + ["Fortunately, only one parse tree is type correct" ^ + Position.str_of (Position.reset_range pos) ^ + ",\nbut you may still want to disambiguate your grammar or your input."])) + else (); report_result ctxt pos [] results') else - report_result ctxt pos - [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @ - (("Ambiguous input, " ^ string_of_int checked_len ^ " terms are type correct" ^ + report_result ctxt pos [] + [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @ + (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^ (if checked_len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map show_term (take limit checked))))))] @@ -419,7 +409,7 @@ val (syms, pos) = Syntax.read_token str; in parse_asts ctxt true root (syms, pos) - |> report_result ctxt pos + |> uncurry (report_result ctxt pos) |> constify end;