--- a/src/Pure/Interface/proof_general.ML Thu Nov 15 23:21:57 2001 +0100
+++ b/src/Pure/Interface/proof_general.ML Thu Nov 15 23:25:01 2001 +0100
@@ -20,7 +20,7 @@
val repeat_undo: int -> unit
val isa_restart: unit -> unit
val init: bool -> unit
- val write_keywords: unit -> unit
+ val write_keywords: string -> unit
end;
structure ProofGeneral: PROOF_GENERAL =
@@ -308,13 +308,11 @@
implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
"\n(provide 'isar-keywords)\n";
-val keywords_file = "isar-keywords.el";
-
in
-fun write_keywords () =
+fun write_keywords s =
(init_outer_syntax ();
- File.write (Path.unpack keywords_file)
+ File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
end;