1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 29 06:03:41 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 29 06:04:01 2004 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.5    val improper_command: string -> string -> string ->
     1.6      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.7 +  val is_keyword: string -> bool
     1.8    val dest_keywords: unit -> string list
     1.9    val dest_parsers: unit -> (string * string * string * bool) list
    1.10    val print_outer_syntax: unit -> unit
    1.11 @@ -204,6 +205,7 @@
    1.12  
    1.13  (* print syntax *)
    1.14  
    1.15 +fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
    1.16  fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
    1.17  
    1.18  fun dest_parsers () =

     2.1 --- a/src/Pure/Syntax/syntax.ML	Thu Apr 29 06:03:41 2004 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Apr 29 06:04:01 2004 +0200
     2.3 @@ -37,6 +37,7 @@
     2.4      PrintRule of 'a * 'a |
     2.5      ParsePrintRule of 'a * 'a
     2.6    type syntax
     2.7 +  val is_keyword: syntax -> string -> bool
     2.8    val extend_log_types: string list -> syntax -> syntax
     2.9    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
    2.10    val extend_const_gram: string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    2.11 @@ -178,6 +179,8 @@
    2.12      tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
    2.13      prtabs: Printer.prtabs}
    2.14  
    2.15 +fun is_keyword (Syntax {lexicon, ...}) = Scan.is_literal lexicon o Symbol.explode;
    2.16 +
    2.17  
    2.18  (* empty_syntax *)
    2.19  
    2.20 @@ -359,12 +362,12 @@
    2.21        warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
    2.22    in
    2.23      if length pts > ! ambiguity_level then
    2.24 -	if ! ambiguity_is_error then
    2.25 -	    error ("Ambiguous input " ^ quote str)
    2.26 -	else
    2.27 -	    (warning ("Ambiguous input " ^ quote str);
    2.28 -	     warning "produces the following parse trees:";
    2.29 -	     seq show_pt pts)
    2.30 +        if ! ambiguity_is_error then
    2.31 +            error ("Ambiguous input " ^ quote str)
    2.32 +        else
    2.33 +            (warning ("Ambiguous input " ^ quote str);
    2.34 +             warning "produces the following parse trees:";
    2.35 +             seq show_pt pts)
    2.36      else ();
    2.37      map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
    2.38    end;