More hacks to variable names for customize (sorry)

5 files changed, 55 insertions, 61 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1d501da1..51b11fbc 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -46,18 +46,18 @@
 (defcustom proof-prog-name-ask-p nil
   "*If non-nil, query user which program to run for the inferior process."
   :type 'boolean
-  :group 'proof)
+  :group 'proof-general)
 
 (defcustom proof-one-command-per-line nil
   "*If non-nil, format for newlines after each proof command in a script."
   :type 'boolean
-  :group 'proof)
+  :group 'proof-general)
 
 (and (featurep 'toolbar)
 (defcustom proof-toolbar-wanted t
   "*Whether to use toolbar in proof mode."
   :type 'boolean
-  :group 'proof))
+  :group 'proof-general))
 
 (defcustom proof-toolbar-follow-mode 'follow
   "*Choice of how point moves with toolbar commands.
@@ -69,7 +69,7 @@ If ignore, point is never moved after toolbar movement commands."
 	  (const :tag "Follow locked region" locked)
 	  (const :tag "Keep locked region displayed" follow)
 	  (const :tag "Never move" ignore))
-  :group 'proof)
+  :group 'proof-general)
 
 
 ;;
@@ -181,7 +181,7 @@ Could come either from proof assistant or Proof General itself."
 
 (defgroup prover-config nil
   "Configuration of Proof General for the prover in use."
-  :group 'proof-internal
+  :group 'proof-general-internals
   :prefix "proof-")
 
 ;; The variables in the "prover-config" (NB: not "proof config"!!)
@@ -196,24 +196,17 @@ Could come either from proof assistant or Proof General itself."
 ;; not liable to work, because the prover specific elisp usually
 ;; overrides with a series of setq's in <assistant>-mode-config type
 ;; functions.  This is why prover-config appears under the
-;; proof-internal group.
-
-;; Note: The XEmacs customization menus would be nicer if the
-;; variables in prover-config group were uniformly renamed
-;; prover-config-* (and similarly for other variables/groups).  
-;; But it's somewhat of a horror in the code!
-
+;; proof-general-internal group.
 
 (defcustom proof-assistant ""
   "Name of the proof assistant Proof General is using.
 This is set automatically by the mode stub defined in proof-site,
-from the name given in proof-internal-assistant-table."
+from the name given in proof-assistant-table."
   :type 'string
   :group 'prover-config)
 
 
 
-
 
 ;;
 ;; 2. The major modes used by Proof General.
@@ -251,7 +244,7 @@ Suggestion: this can be set in the script mode configuration."
 ;; 3. Configuration for menus, user-level commands, etc.
 ;;
 
-(defcustom proof-www-home-page ""
+(defcustom proof-asssistant-home-page ""
   "Web address for information on proof assistant"
   :type 'string
   :group 'prover-config)
@@ -439,7 +432,7 @@ This is used to handle nested goals allowed by some provers."
 (defgroup proof-shell nil
   "Settings for output from the proof assistant in the proof shell."
   :group 'prover-config
-  :prefix "proof-")
+  :prefix "proof-shell-")
 
 
 ;; 
@@ -661,13 +654,13 @@ data triggered by `proof-shell-retract-files-regexp'."
   "Root name for proof script mode.  
 Used internally and in menu titles."
   :type 'string
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
-(defcustom proof-general-home-page
+(defcustom proof-proof-general-home-page
   "http://www.dcs.ed.ac.uk/home/proofgen"
   "*Web address for Proof General"
   :type 'string
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
 ;; FIXME: da: could we put these into another keymap already?
 ;; FIXME: da: it's offensive to experienced users to rebind global stuff
@@ -683,7 +676,7 @@ Used internally and in menu titles."
 Elements of the list are tuples (k . f) 
 where `k' is a keybinding (vector) and `f' the designated function."
   :type 'sexp
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
 
 
@@ -712,7 +705,7 @@ return a non-nil value. Then (actf cmd string) is invoked. See the
 documentation of `proof-shell-process-output' for the required
 output format."
   :type '(cons (function function))
-  :group 'prover-config)
+  :group 'proof-shell)
 
 (defcustom proof-activate-scripting-hook nil
   "Hook run when a buffer is switched into scripting mode.
@@ -721,7 +714,7 @@ The current buffer will be the newly active scripting buffer.
 This hook may be useful for synchronizing with the proof
 assistant, for example, to switch to a new theory."
   :type '(repeat function)
-  :group 'prover-config)
+  :group 'proof-script)
 
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 8fabb2b8..a45b45a2 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1285,9 +1285,9 @@ Start up the proof assistant if necessary."
 (defvar proof-help-menu
   `("Help"
     [,(concat proof-assistant " web page")
-     (browse-url proof-www-home-page) t]
+     (browse-url proof-assistant-home-page) t]
     ["Proof General home page"
-     (browse-url proof-general-home-page) t]
+     (browse-url proof-proof-general-home-page) t]
     ["Proof General Info" proof-info-mode t]
     )
   "The Help Menu in Script Management.")
@@ -1506,9 +1506,10 @@ finish setup which depends on specific proof assistant configuration."
 			   ;; older/non-existent customize doesn't have 
 			   ;; this function.  
 			   (if (fboundp 'customize-menu-create)
-			       (list (customize-menu-create 'proof)
-				     (customize-menu-create 'proof-internal
-							    "Internals"))
+			       (list (customize-menu-create 'proof-general)
+				     (customize-menu-create
+				      'proof-general-internals
+				      "Internals"))
 			     nil)
 			   ;; end UGLY COMPATIBILTY HACK
 			   )))
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 0b4eb909..8e775c70 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -18,7 +18,7 @@
 ;; end UGLY COMPATIBILITY HACK
 
 
-(defgroup proof nil
+(defgroup proof-general nil
   "Customization of Proof General."
   :group 'external
   :group 'processes
@@ -30,14 +30,14 @@
 ;; configuration to different proof assistants.
 ;; This is for development purposes rather than
 ;; user-level customization, so this group does
-;; not belong to 'proof (or any other group).
-(defgroup proof-internal nil
+;; not belong to 'proof-general (or any other group).
+(defgroup proof-general-internals nil
   "Customization of Proof General internals."
   :prefix "proof-")
 
 
 ;; Master table of supported assistants.
-(defcustom proof-internal-assistant-table
+(defcustom proof-assistant-table
   '((isa	"Isabelle"	"\\.ML$\\|\\.thy$")
     (lego	"LEGO"		"\\.l$")
     (coq	"Coq"		"\\.v$"))
@@ -58,12 +58,12 @@ directory and elisp file for the mode, which will be
 where `<proof-directory-home>/' is the value of the
 variable proof-directory-home."
   :type '(repeat (list symbol string string))
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
 
 ;; Directories
 
-(defcustom proof-internal-home-directory
+(defcustom proof-home-directory
   ;; FIXME: make sure compiling does not evaluate next expression.
   (or (getenv "PROOFGENERAL_HOME") 
       (let ((curdir 
@@ -76,19 +76,19 @@ Default value taken from environment variable PROOFGENERAL_HOME if set,
 otherwise based on where the file proof-site was loaded from.
 You can use customize to set this variable."
   :type 'directory
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
-(defcustom proof-internal-images-directory
-  (concat proof-internal-home-directory "images/")
+(defcustom proof-images-directory
+  (concat proof-home-directory "images/")
     "*Where Proof General image files are installed. Ends with slash."
   :type 'directory
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
-(defcustom proof-internal-info-directory
-  (concat proof-internal-home-directory "doc/")
+(defcustom proof-info-directory
+  (concat proof-home-directory "doc/")
   "*Where Proof General Info files are installed."
   :type 'directory
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
 ;; Add the info directory to the end of Emacs Info path if need be.
 ;; It's easier to do this after Info has loaded because of the
@@ -96,10 +96,10 @@ You can use customize to set this variable."
 
 (eval-after-load
  "info"
- '(or (member proof-internal-info-directory Info-directory-list)
+ '(or (member proof-info-directory Info-directory-list)
      (progn
        (setq Info-directory-list
-	     (cons proof-internal-info-directory
+	     (cons proof-info-directory
 		   Info-directory-list))
        ;; Clear cache of info dir
        (setq Info-dir-contents nil))))
@@ -108,13 +108,13 @@ You can use customize to set this variable."
 ;; Might be nicer to have a boolean for each supported assistant.
 (defcustom proof-assistants
   (mapcar (lambda (astnt) (car astnt))
-	  proof-internal-assistant-table)
+	  proof-assistant-table)
   (concat
    "*Choice of proof assitants to use with Proof General.
 A list of symbols chosen from:" 
    (apply 'concat (mapcar (lambda (astnt) 
 			    (concat " '" (symbol-name (car astnt))))
-			  proof-internal-assistant-table)) 
+			  proof-assistant-table)) 
 ".\nEach proof assistant defines its own instance of Proof General,
 providing session control, script management, etc.  Proof General
 will be started automatically for the assistants chosen here.
@@ -124,12 +124,12 @@ NOTE: to change proof assistant, you must start a new Emacs session.")
   :type (cons 'set 
 	      (mapcar (lambda (astnt)
 			(list 'const ':tag (car (cdr astnt)) (car astnt)))
-		      proof-internal-assistant-table))
-  :group 'proof)
+		      proof-assistant-table))
+  :group 'proof-general)
 
 ;; Extend load path for the generic files.
 (let ((proof-lisp-path
-       (concat proof-internal-home-directory "generic/")))
+       (concat proof-home-directory "generic/")))
   (or (member proof-lisp-path load-path)
       (setq load-path
 	    (cons proof-lisp-path load-path))))
@@ -139,8 +139,8 @@ NOTE: to change proof assistant, you must start a new Emacs session.")
 ;; FIXME: this doesn't work quite right.  We want to test
 ;; whether we are running during a compilation.  How?
 ; (eval-when-compile
-;  (dolist (assistant proof-internal-assistant-table)
-;    (let ((path (concat proof-internal-home-directory
+;  (dolist (assistant proof-assistant-table)
+;    (let ((path (concat proof-home-directory
 ;			(concat (symbol-name (car assistant)) "/"))))
 ;      (or (member path load-path)
 ;	  (setq load-path
@@ -156,9 +156,9 @@ NOTE: to change proof assistant, you must start a new Emacs session.")
 	  (or 
 	   (cdr-safe 
 	    (assoc assistant
-		   proof-internal-assistant-table))
+		   proof-assistant-table))
 	   (error "proof-site: symbol " (symbol-name assistant) 
-		  "is not in proof-internal-assistant-table")))
+		  "is not in proof-assistant-table")))
 	 (assistant-name (car nameregexp))
 	 (regexp	 (car (cdr nameregexp)))
 	 (sname		 (symbol-name assistant))
@@ -184,12 +184,12 @@ NOTE: to change proof assistant, you must start a new Emacs session.")
 	      (defgroup ,cusgrp nil
 		,(concat "Customization of " assistant-name
 			 " specific settings for Proof General.")
-		:group 'proof)
+		:group 'proof-general)
 	      ;; Set the proof-assistant configuration variable
 	      (setq proof-assistant ,assistant-name)
 	      ;; Extend the load path, load the real mode and invoke it.
 	      (setq load-path 
-		    (cons (concat proof-internal-home-directory ,elisp-dir "/")
+		    (cons (concat proof-home-directory ,elisp-dir "/")
 			  load-path))
 	      (load-library ,elisp-file)
 	      (,proofgen-mode))))
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 85a349e6..025431d6 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -25,10 +25,10 @@ Gif filename depends on colour depth of display."
   (cond
    ((and window-system (featurep 'jpeg) (not nojpeg))
     (vector 'jpeg :file
-	    (concat proof-internal-images-directory name ".jpg")))
+	    (concat proof-images-directory name ".jpg")))
    ((and window-system (featurep 'gif))
     (vector 'gif :file
-	    (concat proof-internal-images-directory 
+	    (concat proof-images-directory 
 		    (concat name
 			    (or (and
 				 (fboundp 'device-pixel-depth)
@@ -64,12 +64,12 @@ inserted."
   :type 'sexp
   :group 'proof-config)
 
-(defcustom proof-internal-display-splash-time 1.5
+(defcustom proof-splash-time 1.5
   "Minimum number of seconds to display splash screen for.
 The splash screen may be displayed for a couple of seconds longer than
 this, depending on how long it takes the machine to initialise proof mode."
   :type 'number
-  :group 'proof-internal)
+  :group 'proof-general-internals)
 
 ;; Would be nice to get rid of this variable, but it's tricky
 ;; to construct a hook function, with a higher order function,
@@ -148,7 +148,7 @@ Only do it if proof-splash-display is nil."
 	  (sit-for 0))
 	(setq proof-splash-timeout-conf
 	      (cons
-	       (add-timeout proof-internal-display-splash-time
+	       (add-timeout proof-splash-time
 			    'proof-splash-remove-screen
 			    winconf)
 	       winconf))))))
@@ -161,7 +161,7 @@ Only do it if proof-splash-display is nil."
 ;; To approximate the best behaviour, we assume that this file is
 ;; loaded by a call to proof-mode.  We display the screen now and add
 ;; a wait procedure temporarily to proof-mode-hook which prevents
-;; redisplay until proof-internal-display-splash-time has elapsed. 
+;; redisplay until proof-splash-time has elapsed. 
 
 ;; Display the screen ASAP...
 (proof-splash-display-screen)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 84a09dad..2686ccb3 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -36,7 +36,7 @@ prover specific buttons, see proof-toolbar.el.")
     (proof-toolbar-restart-icon "restart"))
   "List of icon variable names and their associated image files.
 A list of lists of the form (VAR IMAGE).  IMAGE is the root name
-for an image file in proof-internal-images-directory.  The toolbar
+for an image file in proof-images-directory.  The toolbar
 code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm
 and chooses the best one for the display properites.")
 
@@ -82,7 +82,7 @@ to the default toolbar."
 	 (lambda (buttons)
 	   (let ((var	(car buttons))
 		 (iconfiles (mapcar (lambda (name)
-				      (concat proof-internal-images-directory
+				      (concat proof-images-directory
 					      name
 					      icontype)) (cdr buttons))))
 	     (set var (toolbar-make-button-list iconfiles))))