Added proof-ready-for-assistant function to help docstring magic.

1 files changed, 50 insertions, 40 deletions

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 74b2d7a4..170c293e 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -187,6 +187,52 @@ Note: to change proof assistant, you must start a new Emacs session.")
 ;	  (setq load-path
 ;		(cons path load-path))))))
 
+(defun proof-ready-for-assistant (assistant-name assistantsym)
+  "Configure PG for ASSISTANT-NAME, symbol ASSISTANTSYM."
+  (let*
+      ((sname		 (symbol-name assistantsym))
+       (cusgrp-rt	 
+	;; Normalized a bit to remove spaces and funny characters
+	;; FIXME UGLY compatibility hack  
+	;; (can use cl macro `substitute' but want to avoid cl here)
+	(if (fboundp 'replace-in-string) 
+	    ;; XEmacs
+	    (replace-in-string (downcase assistant-name) "/\\|[ \t]+" "-")
+	  ;; FSF
+	  (subst-char-in-string 
+	   ?/ ?\- 
+	   (subst-char-in-string ?\ ?\- (downcase assistant-name)))))
+	;; END compatibility hack
+       (cusgrp	 (intern cusgrp-rt))
+       (cus-internals  (intern (concat cusgrp-rt "-config")))
+       ;; NB: Dir name for each prover is the same as its symbol name!
+       (elisp-dir    sname))
+    (eval `(progn
+       ;; Make a customization group for this assistant
+       (defgroup ,cusgrp nil
+	 ,(concat "Customization of user options for " assistant-name
+		  " Proof General.")
+	 :group 'proof-general)
+       ;; And another one for internals
+       (defgroup ,cus-internals nil
+	 ,(concat "Customization of internal settings for "
+		  assistant-name " configuration.")
+	 :group 'proof-general-internals
+	 :prefix ,(concat sname "-"))
+    
+       ;; Set the proof-assistant configuration variables
+       ;; NB: tempting to use customize-set-variable: wrong!
+       ;; Here we treat customize as extended docs for these
+       ;; variables.
+       (setq proof-assistant-cusgrp (quote ,cusgrp))
+       (setq proof-assistant-internals-cusgrp (quote ,cus-internals))
+       (setq proof-assistant ,assistant-name)
+       (setq proof-assistant-symbol (quote ,assistantsym))
+       ;; Extend the load path
+       (setq load-path 
+	     (cons (concat proof-home-directory ,elisp-dir "/")
+		   load-path))))))
+
 ;; Now add auto-loads and load-path elements to support the 
 ;; proof assistants selected, and define a stub 
 (let ((assistants proof-assistants))
@@ -205,24 +251,9 @@ Note: to change proof assistant, you must start a new Emacs session.")
 	 (sname		 (symbol-name assistant))
 	 ;; NB: File name for each prover is the same as its symbol name!
 	 (elisp-file   sname)
-	 ;; NB: Dir name for each prover is the same as its symbol name!
-	 (elisp-dir    sname)
 	 ;; NB: Mode name for each prover is <symbol name>-mode!
 	 (proofgen-mode  (intern (concat sname "-mode")))
 	 ;; NB: Customization group for each prover is its l.c.'d name!
-	 (cusgrp-rt	 
-	  ;; Normalized a bit to remove spaces and funny characters
-	  ;; FIXME UGLY compatibility hack  
-	  ;; (can use cl macro `substitute' but want to avoid cl here)
-	  (if (fboundp 'replace-in-string) 
-	      ;; XEmacs
-	      (replace-in-string (downcase assistant-name) "/\\|[ \t]+" "-")
-	    ;; FSF
-	    (subst-char-in-string ?/ ?\- 
-	     (subst-char-in-string ?\ ?\- (downcase assistant-name)))))
-	 ;; END compatibility hack
-	 (cusgrp	 (intern cusgrp-rt))
-	 (cus-internals  (intern (concat cusgrp-rt "-config")))
 
 	 ;; Stub to do some automatic initialization and load
 	 ;; the specific code.
@@ -233,7 +264,6 @@ Note: to change proof assistant, you must start a new Emacs session.")
 		 assistant-name
 		 ".\nThis is a stub which loads the real function.")
 	      (interactive)
-
 	      ;; Give a message and stop loading if proof-assistant is
 	      ;; already set: things go wrong if proof general is
 	      ;; loaded for more than one prover.
@@ -248,30 +278,10 @@ Note: to change proof assistant, you must start a new Emacs session.")
 		      " Proof General error: Proof General already in use for "
 		      proof-assistant))))
 	       (t
-		;; Make a customization group for this assistant
-		(defgroup ,cusgrp nil
-		  ,(concat "Customization of user options for " assistant-name
-			   " Proof General.")
-		  :group 'proof-general)
-		;; And another one for internals
-		(defgroup ,cus-internals nil
-		  ,(concat "Customization of internal settings for "
-			   assistant-name " configuration.")
-		  :group 'proof-general-internals
-		  :prefix ,(concat sname "-"))
-		
-		;; Set the proof-assistant configuration variables
-		;; NB: tempting to use customize-set-variable: wrong!
-		;; Here we treat customize as extended docs for these
-		;; variables.
-		(setq proof-assistant-cusgrp (quote ,cusgrp))
-		(setq proof-assistant-internals-cusgrp (quote ,cus-internals))
-		(setq proof-assistant ,assistant-name)
-		(setq proof-assistant-symbol (quote ,assistant))
-		;; Extend the load path, load the real mode and invoke it.
-		(setq load-path 
-		      (cons (concat proof-home-directory ,elisp-dir "/")
-			    load-path))
+		;; prepare variables and load path
+		(proof-ready-for-assistant ,assistant-name 
+					   (quote ,assistant))
+		;; load the real mode and invoke it. 
 		(load-library ,elisp-file)
 		(,proofgen-mode))))))