--- 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;