pbp-mode -> goals-mode

3 files changed, 28 insertions, 28 deletions

diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index 067cde0d..d59d4394 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -13,10 +13,10 @@
 (require 'proof)
 
 (defvar proof-easy-config-derived-modes-table
-  '((""         "script" proof-mode (proof-config-done))
-    ("shell"    "shell"  proof-shell-mode (proof-shell-config-done))
-    ("response" "resp"   proof-response-mode (proof-response-config-done))
-    ("goals"	"goals"  pbp-mode (proof-goals-config-done)))
+  '((""         "script"     proof-mode (proof-config-done))
+    ("shell"    "shell"      proof-shell-mode (proof-shell-config-done))
+    ("response" "response"   proof-response-mode (proof-response-config-done))
+    ("goals"	"goals"      proof-goals-mode (proof-goals-config-done)))
   "A list of (PREFIXSYM SUFFIXNAME PARENT MODEBODY) for derived modes.")
 
 (defun proof-easy-config-define-derived-modes ()
@@ -76,9 +76,7 @@
      (proof-easy-config-check-setup ,sym ,name)
      (setq
       ,@body)
-     (proof-easy-config-define-derived-modes)
-     ;; FIXME: Non-uniformity in current code
-     (setq proof-mode-for-goals proof-mode-for-pbp)))
+     (proof-easy-config-define-derived-modes)))
   
 ;; 
 (provide 'proof-easy-config)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 5814172e..a4936b9d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -262,7 +262,7 @@ Does nothing if proof assistant is already running."
 	      (set-buffer proof-goals-buffer)
 	      (and (fboundp 'toggle-enable-multibyte-characters)
 		   (toggle-enable-multibyte-characters -1))
-	      (funcall proof-mode-for-pbp))
+	      (funcall proof-mode-for-goals))
 	  (switch-to-buffer proof-shell-buffer)
 	  (error "%s process exited!" proc)))
       (message 
@@ -863,6 +863,8 @@ Then we call `proof-shell-handle-error-or-interrupt-hook'."
     (proof-script-clear-queue-spans) 
     (setq proof-action-list nil)
     (proof-release-lock err-or-int)
+    ;; Make sure that prover is outputting data now.
+
     ;; New: this is called for interrupts too.
     (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))
 
@@ -1926,35 +1928,35 @@ processing."
 ;;
 
 
-(eval-and-compile			; to define pbp-mode-map
-(define-derived-mode pbp-mode proof-universal-keys-only-mode
+(eval-and-compile			; to define proof-goals-mode-map
+(define-derived-mode proof-goals-mode proof-universal-keys-only-mode
   proof-general-name 
   "Mode for goals display.  
 May enable proof-by-pointing or similar features.
-\\{pbp-mode-map}"
-  ;; defined-derived-mode pbp-mode initialises pbp-mode-map
-  (setq proof-buffer-type 'pbp)
+\\{proof-goals-mode-map}"
+  ;; defined-derived-mode proof-goals-mode initialises proof-goals-mode-map
+  (setq proof-buffer-type 'goals)
   (cond 
    ((string-match "XEmacs" emacs-version)
-    (define-key pbp-mode-map [(button2)] 'pbp-button-action)
-    (define-key pbp-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
+    (define-key proof-goals-mode-map [(button2)] 'pbp-button-action)
+    (define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
     ;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well.
     ;; Actually we better hadn't, people like to use it for cut and paste.
-    ;; (define-key pbp-mode-map [(button1)] 'pbp-button-action)
-    ;; (define-key pbp-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
-    (define-key pbp-mode-map [(button3)] 'pbp-yank-subterm))
+    ;; (define-key proof-goals-mode-map [(button1)] 'pbp-button-action)
+    ;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
+    (define-key proof-goals-mode-map [(button3)] 'pbp-yank-subterm))
    (t
-    (define-key pbp-mode-map [mouse-2] 'pbp-button-action)
-    (define-key pbp-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
-    ;; (define-key pbp-mode-map [mouse-1] 'pbp-button-action)
-    ;; (define-key pbp-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
-   (define-key pbp-mode-map [mouse-3] 'pbp-yank-subterm)))
-  (define-key pbp-mode-map [q] 'bury-buffer)
-  (easy-menu-add proof-goals-mode-menu pbp-mode-map)
+    (define-key proof-goals-mode-map [mouse-2] 'pbp-button-action)
+    (define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
+    ;; (define-key proof-goals-mode-map [mouse-1] 'pbp-button-action)
+    ;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
+   (define-key proof-goals-mode-map [mouse-3] 'pbp-yank-subterm)))
+  (define-key proof-goals-mode-map [q] 'bury-buffer)
+  (easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
   (erase-buffer)))
 
 (easy-menu-define proof-goals-mode-menu
-		  pbp-mode-map
+		  proof-goals-mode-map
 		  "Menu for Proof General goals buffer."
 		  (cons proof-general-name proof-shared-menu))
 
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index bdc1175a..6ebff0ad 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -87,8 +87,8 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol"))
 			      (or proof-mode-for-script
 				  ;; FIXME: next one only correct for isabelle
 				  (intern (concat assistant "-proofscript-mode")))
-			      (or  proof-mode-for-pbp
-				   (intern (concat assistant "-pbp-mode")))))
+			      (or  proof-mode-for-goals
+				   (intern (concat assistant "-goals-mode")))))
 	     (all-xs-modes   (append xs-std-modes xs-xtra-modes))
 	     (am-entry       (list proof-xsym-extra-modes t 
 				   `(quote ,xs-lang)))