src/Pure/Syntax/syntax.ML

   datatype 'a trrule =
     ParseRule of 'a * 'a |
     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
   val extend_consts: string list -> syntax -> syntax
   val extend_trfuns:

     print_ruletab: ruletab,
     print_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     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 *)
 
 val empty_syntax =
   Syntax {

 
     fun show_pt pt =
       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;