# HG changeset patch
# User wenzelm
# Date 1005863101 -3600
# Node ID e3efc5c9f267fde37d395c8a9f6fde14b65edc04
# Parent  dda8c04a8fb49d15819725abd31a0f332efa4b2f
write_keywords: string argument (logic name);

diff -r dda8c04a8fb4 -r e3efc5c9f267 src/Pure/Interface/proof_general.ML
--- 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;