Renamed some configuration variables for uniformity, see CHANGES.

9 files changed, 35 insertions, 32 deletions

diff --git a/CHANGES b/CHANGES
index e5938e86..b3ae194b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,23 +8,21 @@ Generic Changes
   New function control-button1 (proof-mouse-track-insert) copies 
   individual commands (highlighted regions) from an open proof.  
   When a proof is closed, it behaves as mouse-track-insert
-  (default XEmacs behaviour of control-button1).  
-  
+  (the default XEmacs behaviour of control-button1).  
 
 * New function C-c C-f (proof-find) to invoke some prover-specific
   mechanism to search for theories.  
 
-* [XEmacs only] Toolbar has five new buttons (State, Context, Info, 
-  Command, Help) which invoke commands previously available on keys/menus.
-  Also a new "Find" button for proof-find.
+* [XEmacs only] Toolbar has six new buttons (State, Context, Info, 
+  Command, Help, Stop) which invoke commands previously available on 
+  keys/menus.   Also a new "Find" button for proof-find.
 
 * [XEmacs only] Toolbar enablers have been added.   
   Buttons are automatically enabled or disabled as appropriate.   
   This requires XEmacs 20.4 or better for reliable working.  
-  
 
 * Menus and keybindings have been reorganized.  
-  Now keybindings invoke same functions as toolbar.
+  Now keybindings invoke the same functions as the toolbar.
 
 * Terminal string now automatically added to command for C-c C-v 
 
@@ -76,5 +74,10 @@ Internal changes for developers to note
   using special character codes is fragile and needs replacing
   in future versions of Proof General!
 
+* Renamed some configuration variables for uniformity:
+    proof-ctxt-string -> proof-context-command
+    proof-help-string -> proof-info-command
+    proof-prf-string  -> proof-showproof-command
+
 * Code cleanups and improvements.
 
diff --git a/coq/coq.el b/coq/coq.el
index 4e6767f2..c84b9719 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -425,13 +425,13 @@
   (setq proof-guess-command-line 'coq-guess-command-line)
 
   ;; Commands sent to proof engine
-  (setq proof-prf-string "Show"
-	proof-ctxt-string "Print All"
+  (setq proof-proof-command "Show"
+	proof-context-command "Print All"
 	proof-goal-command "Goal %s."
 	proof-save-command "Save %s."
 	proof-find-theorems-command "Search %s."
 ;; FIXME da: Does Coq have a help or about command?
-;;	proof-help-string "Help"
+;;	proof-info-command "Help"
 	proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
diff --git a/generic/proof-config.el b/generic/proof-config.el
index aab2e4d6..2a563855 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -437,17 +437,17 @@ command line options.  For an example, see coq/coq.el."
   :type 'string
   :group 'prover-config)
 
-(defcustom proof-ctxt-string ""
+(defcustom proof-context-command ""
   "Command to display the context in proof assistant."
   :type 'string
   :group 'prover-config)
 
-(defcustom proof-help-string ""
-  "Command to ask for help in proof assistant."
+(defcustom proof-info-command ""
+  "Command to ask for help or information in the proof assistant."
   :type 'string
   :group 'prover-config)
 
-(defcustom proof-prf-string ""
+(defcustom proof-proof-command ""
   "Command to display proof state in proof assistant."
   :type 'string
   :group 'prover-config)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e6938743..a3f0498e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1510,14 +1510,14 @@ Start up the proof assistant if necessary."
 
 (proof-define-assistant-command proof-prf  
   "Show the current proof state."
-  proof-prf-string)
+  proof-proof-command)
 (proof-define-assistant-command proof-ctxt 
   "Show the current context."
-  proof-ctxt-string)
+  proof-context-command)
 (proof-define-assistant-command proof-help 
   "Show a help or information message from the proof assistant.
 Typically, a list of syntax of commands available."
-  proof-help-string)
+  proof-info-command)
 
 ;;
 ;; Commands which require an argument, and maybe affect the script.
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 3051764d..805c0dfb 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -27,7 +27,7 @@
 ;; in proof-toolbar-setup.
 
 ;; FIXME: consider automatically disabling buttons which are
-;; not configured for the prover, e.g. if proof-help-string is
+;; not configured for the prover, e.g. if proof-info-command is
 ;; not set, then the Info button should not be show. 
 
 ;; FIXME: In the future, add back the enabler functions.
diff --git a/isa/isa.el b/isa/isa.el
index 2bb32142..d84a42b5 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -128,11 +128,11 @@ no regular or easily discernable structure."
    proof-indent-commands-regexp	(proof-ids-to-regexp isa-keywords)
    
    ;; proof engine commands
-   proof-prf-string		"pr()"
+   proof-proof-command		"pr()"
    proof-goal-command		"Goal \"%s\";"
    proof-save-command		"qed \"%s\";"
-   proof-ctxt-string		"ProofGeneral.show_context()"
-   proof-help-string		"ProofGeneral.help()"
+   proof-context-command		"ProofGeneral.show_context()"
+   proof-info-command		"ProofGeneral.help()"
    proof-kill-goal-command	"ProofGeneral.kill_goal();"
    proof-find-theorems-command  "ProofGeneral.thms_containing [\"%s\"]"
    ;; command hooks
diff --git a/isar/isar.el b/isar/isar.el
index 0b01bd34..1c529bc3 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -158,11 +158,11 @@
    proof-save-with-hole-regexp  isar-save-with-hole-regexp
    proof-indent-commands-regexp	isar-indent-regexp
    ;; proof engine commands
-   proof-prf-string		"pr"
+   proof-proof-command		"pr"
    proof-goal-command		"lemma \"%s\";"
    proof-save-command		"qed"
-   proof-ctxt-string		"print_context"
-   proof-help-string		"help"
+   proof-context-command		"print_context"
+   proof-info-command		"help"
    proof-kill-goal-command	"kill_proof;"
    proof-find-theorems-command  "thms_containing %s;"
    ;; command hooks
diff --git a/lego/lego.el b/lego/lego.el
index a8b5276e..5930f501 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -349,11 +349,11 @@ Checks the width in the `proof-goals-buffer'"
 
   (setq proof-mode-for-script 'lego-mode)
 
-  (setq proof-prf-string "Prf"
+  (setq proof-proof-command "Prf"
 	proof-goal-command "Goal %s;"
 	proof-save-command "Save %s;"
-	proof-ctxt-string "Ctxt"
-	proof-help-string "Help")
+	proof-context-command "Ctxt"
+	proof-info-command "Help")
 
   (setq proof-goal-command-p 'lego-goal-command-p
 	proof-count-undos-fn 'lego-count-undos
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 14f2b8f3..2c3e44ef 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -386,12 +386,12 @@ Given is the first SPAN which needs to be undone."
   (setq proof-assistant-home-page plastic-www-home-page)
   (setq proof-mode-for-script 'plastic-mode)
 
-  (setq proof-prf-string   (concat plastic-lit-string " &S PrfCtxt")
-	proof-goal-command (concat plastic-lit-string " Claim %s;")
-	proof-save-command (concat plastic-lit-string " Save %s;") ;; analogue? 
-	proof-ctxt-string  (concat plastic-lit-string " &S Ctxt 20")
+  (setq proof-showproof-command  (concat plastic-lit-string " &S PrfCtxt")
+	proof-goal-command   (concat plastic-lit-string " Claim %s;")
+	proof-save-command   (concat plastic-lit-string " Save %s;") ;; analogue? 
+	proof-context-command  (concat plastic-lit-string " &S Ctxt 20")
 	   ;; show 20 things; see ^c+C...
-	proof-help-string  (concat plastic-lit-string " &S Help"))
+	proof-info-command   (concat plastic-lit-string " &S Help"))
 
   (setq proof-goal-command-p 'plastic-goal-command-p
 	proof-count-undos-fn 'plastic-count-undos