Added 'ambiguity_is_error' flag, which, if set, makes the parser fail,
rather than just issue a warning, when the input parsed is ambiguous.
--- a/src/Pure/Syntax/syntax.ML Fri Aug 29 18:39:47 2003 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun Aug 31 21:24:29 2003 +0200
@@ -61,11 +61,13 @@
val simple_string_of_typ: typ -> string
val simple_pprint_typ: typ -> pprint_args -> unit
val ambiguity_level: int ref
+ val ambiguity_is_error: bool ref
end;
structure Syntax: SYNTAX =
struct
+val ambiguity_is_error = ref false
(** tables of translation functions **)
@@ -350,9 +352,12 @@
warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
in
if length pts > ! ambiguity_level then
- (warning ("Ambiguous input " ^ quote str);
- warning "produces the following parse trees:";
- seq show_pt pts)
+ if ! ambiguity_is_error then
+ error ("Ambiguous input " ^ quote str)
+ else
+ (warning ("Ambiguous input " ^ quote str);
+ warning "produces the following parse trees:";
+ seq show_pt pts)
else ();
map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
end;