Added 'ambiguity_is_error' flag, which, if set, makes the parser fail,
authorskalberg
Sun Aug 31 21:24:29 2003 +0200 (2003-08-31)
changeset 1417706b19a7e675a
parent 14176 716fec31f9ea
child 14178 14a12da7288e
Added 'ambiguity_is_error' flag, which, if set, makes the parser fail,
rather than just issue a warning, when the input parsed is ambiguous.
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Aug 29 18:39:47 2003 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Aug 31 21:24:29 2003 +0200
     1.3 @@ -61,11 +61,13 @@
     1.4    val simple_string_of_typ: typ -> string
     1.5    val simple_pprint_typ: typ -> pprint_args -> unit
     1.6    val ambiguity_level: int ref
     1.7 +  val ambiguity_is_error: bool ref
     1.8  end;
     1.9  
    1.10  structure Syntax: SYNTAX =
    1.11  struct
    1.12  
    1.13 +val ambiguity_is_error = ref false
    1.14  
    1.15  (** tables of translation functions **)
    1.16  
    1.17 @@ -350,9 +352,12 @@
    1.18        warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
    1.19    in
    1.20      if length pts > ! ambiguity_level then
    1.21 -      (warning ("Ambiguous input " ^ quote str);
    1.22 -       warning "produces the following parse trees:";
    1.23 -       seq show_pt pts)
    1.24 +	if ! ambiguity_is_error then
    1.25 +	    error ("Ambiguous input " ^ quote str)
    1.26 +	else
    1.27 +	    (warning ("Ambiguous input " ^ quote str);
    1.28 +	     warning "produces the following parse trees:";
    1.29 +	     seq show_pt pts)
    1.30      else ();
    1.31      map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
    1.32    end;