# HG changeset patch
# User wenzelm
# Date 1191702717 -7200
# Node ID b38d16db880432352644b4f5ac037fa5a72b0d64
# Parent  711142251c813f16eeff0f6bd4dfa3b172a85557
removed obsolete write_keywords;

diff -r 711142251c81 -r b38d16db8804 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 22:07:19 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 22:31:57 2007 +0200
@@ -11,7 +11,6 @@
   val init: bool -> unit
   val init_outer_syntax: unit -> unit
   val sendback: string -> Pretty.T list -> unit
-  val write_keywords: string -> unit
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
@@ -285,41 +284,4 @@
        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
        Isar.sync_main ());
 
-
-
-(** generate elisp file for keyword classification **)
-
-local
-
-val regexp_meta = member (op =) (explode ".*+?[]^$");
-val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c);
-
-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
-  (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
-
-fun make_elisp_syntax (keywords, commands) =
-  ";;\n\
-  \;; Keyword classification tables for Isabelle/Isar.\n\
-  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
-  \;;\n\
-  \;; $" ^ "Id$\n\
-  \;;\n" ^
-  defconst "major" (map #1 commands) ^
-  defconst "minor" (filter Syntax.is_identifier keywords) ^
-  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
-  "\n(provide 'isar-keywords)\n";
-
-in
-
-fun write_keywords s =
- (init_outer_syntax ();
-  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^ ".el"))
-    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
-
 end;
-
-end;