--- 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 ***
--- 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
--- 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
--- 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
--- 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 *}
--- 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 *}
--- 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 {*
--- 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 #>
--- 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;
--- 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;