pbp-mode -> goals-mode

4 files changed, 20 insertions, 19 deletions

diff --git a/coq/coq.el b/coq/coq.el
index a636a58f..408ffc76 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -15,7 +15,7 @@
 
 (eval-and-compile
   (mapcar (lambda (f) (autoload f "proof-shell"))
-	    '(pbp-mode proof-shell-config-done))) 
+	    '(proof-goals-mode proof-shell-config-done))) 
 
 ; Configuration
 
@@ -115,9 +115,9 @@
    (coq-mode-config)))
 
 (eval-and-compile
-  (define-derived-mode coq-pbp-mode pbp-mode
+  (define-derived-mode coq-goals-mode proof-goals-mode
     "CoqGoals" nil
-    (coq-pbp-mode-config)))
+    (coq-goals-mode-config)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Code that's coq specific                                      ;;
@@ -397,8 +397,9 @@ This is specific to coq-mode."
 
 (defun coq-pre-shell-start ()
   (setq proof-prog-name coq-prog-name)
-  (setq proof-mode-for-shell 'coq-shell-mode)
-  (setq proof-mode-for-pbp 'coq-pbp-mode)
+  (setq proof-mode-for-shell    'coq-shell-mode)
+  (setq proof-mode-for-goals    'coq-goals-mode)
+  (setq proof-mode-for-response 'coq-response-mode)
 )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -526,7 +527,7 @@ This is specific to coq-mode."
 
   (proof-shell-config-done))
 
-(defun coq-pbp-mode-config ()
+(defun coq-goals-mode-config ()
   (setq pbp-change-goal "Show %s.")
   (setq pbp-error-regexp coq-error-regexp)
   (coq-init-syntax-table)
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index b1f7e1c3..1740a100 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -129,7 +129,7 @@
   "Isabelle Demo response" nil
   (proof-response-config-done))
 
-(define-derived-mode demoisa-goals-mode pbp-mode
+(define-derived-mode demoisa-goals-mode proof-goals-mode
   "Isabelle Demo goals" nil
   (proof-goals-config-done))
 
@@ -152,6 +152,6 @@
   (setq proof-prog-name		isabelledemo-prog-name)
   (setq proof-mode-for-shell    'demoisa-shell-mode)
   (setq proof-mode-for-response 'demoisa-response-mode)
-  (setq proof-mode-for-pbp	'demoisa-goals-mode))
+  (setq proof-mode-for-goals	'demoisa-goals-mode))
 
 (provide 'demoisa)
diff --git a/isa/isa.el b/isa/isa.el
index 35eadc18..18c91948 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -342,9 +342,9 @@ proof-shell-retract-files-regexp."
   (isa-response-mode-config)))
 
 (eval-and-compile			; to define vars for byte comp.
-(define-derived-mode isa-pbp-mode pbp-mode
+(define-derived-mode isa-goals-mode proof-goals-mode
   "Isabelle goals" nil
-  (isa-pbp-mode-config)))
+  (isa-goals-mode-config)))
 
 (eval-and-compile			; to define vars for byte comp.
 (define-derived-mode isa-proofscript-mode proof-mode
@@ -567,7 +567,7 @@ you will be asked to retract the file or process the remainder of it."
 (defun isa-pre-shell-start ()
   (setq proof-prog-name		isabelle-prog-name)
   (setq proof-mode-for-shell    'isa-shell-mode)
-  (setq proof-mode-for-pbp	'isa-pbp-mode)
+  (setq proof-mode-for-goals	'isa-goals-mode)
   (setq proof-mode-for-response 'isa-response-mode))
 
 (defun isa-mode-config ()
@@ -606,8 +606,8 @@ you will be asked to retract the file or process the remainder of it."
   (isa-init-output-syntax-table)
   (proof-response-config-done))
 
-(defun isa-pbp-mode-config ()
-  ;; FIXME: next two broken, of course, as is all PBP everywhere.
+(defun isa-goals-mode-config ()
+  ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO.
   (setq pbp-change-goal "Show %s.")	
   (setq pbp-error-regexp proof-shell-error-regexp)
   (isa-init-output-syntax-table)
diff --git a/isar/isar.el b/isar/isar.el
index db4ed62e..e7798739 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -31,7 +31,7 @@
 
 
 ;;; variable: proof-analyse-using-stack
-;;;    proof-locked-region-empty-p, proof-shell-insert, pbp-mode,
+;;;    proof-locked-region-empty-p, proof-shell-insert, proof-goals-mode,
 ;;;    proof-complete-buffer-atomic, proof-shell-invisible-command,
 ;;;    prev-span, span-property, next-span, proof-unprocessed-begin,
 ;;;    proof-config-done, proof-shell-config-done
@@ -361,9 +361,9 @@ proof-shell-retract-files-regexp."
   (isar-response-mode-config)))
 
 (eval-and-compile			; to define vars for byte comp.
-(define-derived-mode isar-pbp-mode pbp-mode
+(define-derived-mode isar-goals-mode proof-goals-mode
   "Isabelle/Isar proofstate" nil
-  (isar-pbp-mode-config)))
+  (isar-goals-mode-config)))
 
 (eval-and-compile			; to define vars for byte comp.
 (define-derived-mode isar-proofscript-mode proof-mode
@@ -542,7 +542,7 @@ proof-shell-retract-files-regexp."
 (defun isar-pre-shell-start ()
   (setq proof-prog-name		isabelle-isar-prog-name)
   (setq proof-mode-for-shell    'isar-shell-mode)
-  (setq proof-mode-for-pbp	'isar-pbp-mode)
+  (setq proof-mode-for-pbp	'isar-goals-mode)
   (setq proof-mode-for-response 'isar-response-mode))
 
 
@@ -593,8 +593,8 @@ proof-shell-retract-files-regexp."
   (isar-outline-setup)
   (proof-response-config-done))
 
-(defun isar-pbp-mode-config ()
-  ;; FIXME: next two broken, of course, as is all PBP everywhere.
+(defun isar-goals-mode-config ()
+  ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO.
   (setq pbp-change-goal "Show %s.")
   (setq pbp-error-regexp proof-shell-error-regexp)
   (isar-init-output-syntax-table)