write_keywords generates outer syntax keyword classification in elisp;

--- a/src/Pure/Interface/proof_general.ML	Mon May 24 21:53:18 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Mon May 24 21:54:34 1999 +0200
@@ -7,6 +7,7 @@
 
 signature PROOF_GENERAL =
 sig
+  val write_keywords: string -> unit
   val setup: (theory -> theory) list
   val init: bool -> unit
 end;
@@ -15,6 +16,40 @@
 struct
 
 
+(** generate keyword classification file **)
+
+local
+
+val regexp_meta = explode ".*+?[]^$";
+val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
+
+fun defconst name strs =
+  "\n(defconst isar-keywords-" ^ name ^
+  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
+
+fun make_elisp_commands commands kind =
+  defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands);
+
+fun make_elisp_syntax (keywords, commands) =
+  ";;\n\
+  \;; Keyword classification tables for Isabelle/Isar.\n\
+  \;; This file generated by Isabelle -- DO NOT EDIT!\n\
+  \;;\n\
+  \;; $Id$\n\
+  \;;\n" ^
+  defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
+  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
+  "\n(provide 'isar-keywords)\n";
+
+in
+
+fun write_keywords file =
+  File.write (Path.unpack file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
+
+end;
+
+
+
 (** compile-time theory setup **)
 
 (* token translations *)