# HG changeset patch
# User wenzelm
# Date 1083211441 -7200
# Node ID e089757b952a68c99e290d75d4fa62fc26fdaeb3
# Parent  708c613370ab13681b1a99555b4a4adc40b39f3d
added is_keyword;

diff -r 708c613370ab -r e089757b952a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 29 06:03:41 2004 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 29 06:04:01 2004 +0200
@@ -51,6 +51,7 @@
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val improper_command: string -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
+  val is_keyword: string -> bool
   val dest_keywords: unit -> string list
   val dest_parsers: unit -> (string * string * string * bool) list
   val print_outer_syntax: unit -> unit
@@ -204,6 +205,7 @@
 
 (* print syntax *)
 
+fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
 
 fun dest_parsers () =
diff -r 708c613370ab -r e089757b952a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Apr 29 06:03:41 2004 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Apr 29 06:04:01 2004 +0200
@@ -37,6 +37,7 @@
     PrintRule of 'a * 'a |
     ParsePrintRule of 'a * 'a
   type syntax
+  val is_keyword: syntax -> string -> bool
   val extend_log_types: string list -> syntax -> syntax
   val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
   val extend_const_gram: string * bool -> (string * typ * mixfix) list -> syntax -> syntax
@@ -178,6 +179,8 @@
     tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
     prtabs: Printer.prtabs}
 
+fun is_keyword (Syntax {lexicon, ...}) = Scan.is_literal lexicon o Symbol.explode;
+
 
 (* empty_syntax *)
 
@@ -359,12 +362,12 @@
       warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
   in
     if length pts > ! ambiguity_level then
-	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)
+        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;