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;