--- a/NEWS Thu Feb 16 17:09:15 2012 +0100
+++ b/NEWS Thu Feb 16 22:18:28 2012 +0100
@@ -36,6 +36,10 @@
"num_position" etc. are mainly used instead (which also include
position information via constraints).
+* Simplified configuration options for syntax ambiguity: see
+"syntax_ambiguity" and "syntax_ambiguity_limit" in isar-ref manual.
+Minor INCOMPATIBILITY.
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 16 17:09:15 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 16 22:18:28 2012 +0100
@@ -980,13 +980,10 @@
text {*
\begin{tabular}{rcll}
- @{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\
+ @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
+ @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
\end{tabular}
- \begin{mldecls}
- @{index_ML Syntax.ambiguity_limit: "int Config.T"} \\ %FIXME attribute
- \end{mldecls}
-
Depending on the grammar and the given input, parsing may be
ambiguous. Isabelle lets the Earley parser enumerate all possible
parse trees, and then tries to make the best out of the situation.
@@ -1003,11 +1000,11 @@
\begin{description}
- \item @{attribute syntax_ambiguity_level} determines the number of
- parser results that are tolerated without printing a detailed
- message.
+ \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 @{ML Syntax.ambiguity_limit} determines the number of
+ \item @{attribute syntax_ambiguity_limit} determines the number of
resulting parse trees that are shown as part of the printed message
in case of an ambiguity.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 16 17:09:15 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 16 22:18:28 2012 +0100
@@ -1154,13 +1154,10 @@
%
\begin{isamarkuptext}%
\begin{tabular}{rcll}
- \indexdef{}{attribute}{syntax\_ambiguity\_level}\hypertarget{attribute.syntax-ambiguity-level}{\hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}} \\
+ \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\_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}
- \begin{mldecls}
- \indexdef{}{ML}{Syntax.ambiguity\_limit}\verb|Syntax.ambiguity_limit: int Config.T| \\ %FIXME attribute
- \end{mldecls}
-
Depending on the grammar and the given input, parsing may be
ambiguous. Isabelle lets the Earley parser enumerate all possible
parse trees, and then tries to make the best out of the situation.
@@ -1177,11 +1174,10 @@
\begin{description}
- \item \hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}} determines the number of
- parser results that are tolerated without printing a detailed
- message.
+ \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 \verb|Syntax.ambiguity_limit| determines the number of
+ \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
in case of an ambiguity.
--- a/src/HOL/Import/proof_kernel.ML Thu Feb 16 17:09:15 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML Thu Feb 16 22:18:28 2012 +0100
@@ -198,7 +198,7 @@
fun smart_string_of_cterm ctxt0 ct =
let
val ctxt = ctxt0
- |> Config.put Syntax.ambiguity_enabled true
+ |> Config.put Syntax.ambiguity "warning" (* FIXME actually "error" (!?) *)
|> Config.put show_brackets false
|> Config.put show_all_types false
|> Config.put show_types false
--- a/src/HOL/MicroJava/J/JListExample.thy Thu Feb 16 17:09:15 2012 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Thu Feb 16 22:18:28 2012 +0100
@@ -8,7 +8,7 @@
imports Eval
begin
-declare [[syntax_ambiguity_level = 100000]]
+declare [[syntax_ambiguity = ignore]]
consts
list_nam :: cnam
--- a/src/HOL/Proofs/Lambda/Commutation.thy Thu Feb 16 17:09:15 2012 +0100
+++ b/src/HOL/Proofs/Lambda/Commutation.thy Thu Feb 16 22:18:28 2012 +0100
@@ -7,7 +7,7 @@
theory Commutation imports Main begin
-declare [[syntax_ambiguity_level = 100]]
+declare [[syntax_ambiguity = ignore]]
subsection {* Basic definitions *}
--- a/src/HOL/Proofs/Lambda/Lambda.thy Thu Feb 16 17:09:15 2012 +0100
+++ b/src/HOL/Proofs/Lambda/Lambda.thy Thu Feb 16 22:18:28 2012 +0100
@@ -7,7 +7,7 @@
theory Lambda imports Main begin
-declare [[syntax_ambiguity_level = 100]]
+declare [[syntax_ambiguity = ignore]]
subsection {* Lambda-terms in de Bruijn notation and substitution *}
--- a/src/HOL/Proofs/Lambda/ListOrder.thy Thu Feb 16 17:09:15 2012 +0100
+++ b/src/HOL/Proofs/Lambda/ListOrder.thy Thu Feb 16 22:18:28 2012 +0100
@@ -7,7 +7,7 @@
theory ListOrder imports Main begin
-declare [[syntax_ambiguity_level = 100]]
+declare [[syntax_ambiguity = ignore]]
text {*
--- a/src/Pure/Isar/attrib.ML Thu Feb 16 17:09:15 2012 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Feb 16 22:18:28 2012 +0100
@@ -503,8 +503,8 @@
register_config Printer.show_types_raw #>
register_config Printer.show_structs_raw #>
register_config Printer.show_question_marks_raw #>
- register_config Syntax.ambiguity_level_raw #>
- register_config Syntax.ambiguity_warnings_raw #>
+ register_config Syntax.ambiguity_raw #>
+ register_config Syntax.ambiguity_limit_raw #>
register_config Syntax_Trans.eta_contract_raw #>
register_config Name_Space.names_long_raw #>
register_config Name_Space.names_short_raw #>
--- a/src/Pure/Syntax/syntax.ML Thu Feb 16 17:09:15 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML Thu Feb 16 22:18:28 2012 +0100
@@ -10,12 +10,10 @@
type operations
val install_operations: operations -> unit
val root: string Config.T
- val ambiguity_enabled: bool Config.T
- val ambiguity_level_raw: Config.raw
- val ambiguity_level: int Config.T
+ val ambiguity_raw: Config.raw
+ val ambiguity: string Config.T
+ val ambiguity_limit_raw: Config.raw
val ambiguity_limit: int Config.T
- val ambiguity_warnings_raw: Config.raw
- val ambiguity_warnings: bool Config.T
val read_token: string -> Symbol_Pos.T list * Position.T
val parse_token: Proof.context -> (XML.tree list -> 'a) ->
Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
@@ -157,19 +155,11 @@
val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
-val ambiguity_enabled =
- Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
-
-val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
-val ambiguity_level = Config.int ambiguity_level_raw;
+val ambiguity_raw = Config.declare "syntax_ambiguity" (fn _ => Config.String "warning");
+val ambiguity = Config.string ambiguity_raw;
-val ambiguity_limit =
- Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
-
-val ambiguity_warnings_raw =
- Config.declare "syntax_ambiguity_warnings" (fn _ => Config.Bool true);
-val ambiguity_warnings =
- Config.bool ambiguity_warnings_raw;
+val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
+val ambiguity_limit = Config.int ambiguity_limit_raw;
(* outer syntax token -- with optional YXML content *)
--- a/src/Pure/Syntax/syntax_phases.ML Thu Feb 16 17:09:15 2012 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Feb 16 22:18:28 2012 +0100
@@ -259,8 +259,6 @@
(* results *)
-fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-
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;
@@ -268,7 +266,7 @@
(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 (ambiguity_msg pos));
+ | _ => error ("Parse error: ambiguous syntax" ^ Position.str_of pos));
(* parse raw asts *)
@@ -288,23 +286,27 @@
(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 warnings = Config.get ctxt Syntax.ambiguity_warnings;
+
val _ =
- if len <= Config.get ctxt Syntax.ambiguity_level then ()
- else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
- else if warnings then
- (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))))
- else ();
+ if len <= 1 orelse ambiguity = "ignore" 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;
-fun parse_raw ctxt root input =
+fun parse_tree ctxt root input =
let
val syn = Proof_Context.syn_of ctxt;
val tr = Syntax.parse_translation syn;
@@ -326,7 +328,7 @@
fun parse_sort ctxt =
Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
(fn (syms, pos) =>
- parse_raw ctxt "sort" (syms, pos)
+ parse_tree ctxt "sort" (syms, pos)
|> report_result ctxt pos
|> decode_sort
|> Type.minimize_sort (Proof_Context.tsig_of ctxt)
@@ -335,7 +337,7 @@
fun parse_typ ctxt =
Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
(fn (syms, pos) =>
- parse_raw ctxt "type" (syms, pos)
+ parse_tree ctxt "type" (syms, pos)
|> report_result ctxt pos
|> decode_typ
handle ERROR msg => parse_failed ctxt pos msg "type");
@@ -351,17 +353,16 @@
Syntax.parse_token ctxt decode markup
(fn (syms, pos) =>
let
- val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
- val ambiguity = length (proper_results results);
+ val results = parse_tree ctxt root (syms, pos) |> map (decode_term ctxt);
+ val parsed_len = length (proper_results results);
- val level = Config.get ctxt Syntax.ambiguity_level;
+ val ambiguity = Config.get ctxt Syntax.ambiguity;
val limit = Config.get ctxt Syntax.ambiguity_limit;
- val warnings = Config.get ctxt Syntax.ambiguity_warnings;
val ambig_msg =
- if ambiguity > 1 andalso ambiguity <= level then
+ if parsed_len > 1 andalso ambiguity = "ignore" then
["Got more than one parse tree.\n\
- \Retry with smaller syntax_ambiguity_level for more information."]
+ \Retry with syntax_ambiguity = \"warning\" for more information."]
else [];
(*brute-force disambiguation via type-inference*)
@@ -369,7 +370,7 @@
handle exn as ERROR _ => Exn.Exn exn;
val results' =
- if ambiguity > 1 then
+ if parsed_len > 1 then
(Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
check results
else results;
@@ -377,15 +378,15 @@
val errs = map snd (failed_results results');
val checked = map snd (proper_results results');
- val len = length checked;
+ val checked_len = length checked;
val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
in
- if len = 0 then
+ if checked_len = 0 then
report_result ctxt pos
[(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
- else if len = 1 then
- (if ambiguity > level andalso warnings then
+ else if checked_len = 1 then
+ (if parsed_len > 1 andalso ambiguity <> "ignore" then
Context_Position.if_visible ctxt warning
("Fortunately, only one parse tree is type correct" ^
Position.str_of (Position.reset_range pos) ^
@@ -394,8 +395,9 @@
else
report_result ctxt pos
[(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
- (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
- (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+ (("Ambiguous input, " ^ 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))))))]
end handle ERROR msg => parse_failed ctxt pos msg kind)
end;