aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 13:30:30 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 13:30:30 +0000
commit5f74f36621d54ae4ba3ec4b24bb5133cbc4f4119 (patch)
treeafd47fa8db82874f5ddcfc412aa114002868f3dd /lego
parent7cfa18895d1369d551d8d2df14cb423082ee1fcd (diff)
goals-mode -> pbp-mode
Diffstat (limited to 'lego')
-rw-r--r--lego/lego.el8
1 files changed, 4 insertions, 4 deletions
diff --git a/lego/lego.el b/lego/lego.el
index 896660d7..2f0dfd5b 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -173,9 +173,9 @@ Activates extended printing routines required for Proof General.")
(lego-init-syntax-table)
(proof-response-config-done)))
-(define-derived-mode lego-pbp-mode pbp-mode
+(define-derived-mode lego-goals-mode proof-goals-mode
"LEGOGoals" "LEGO Proof State"
- (lego-pbp-mode-config))
+ (lego-goals-mode-config))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -339,7 +339,7 @@ Checks the width in the `proof-goals-buffer'"
(setq proof-prog-name lego-prog-name
proof-mode-for-shell 'lego-shell-mode
proof-mode-for-response 'lego-response-mode
- proof-mode-for-pbp 'lego-pbp-mode))
+ proof-mode-for-goals 'lego-goals-mode))
(defun lego-mode-config ()
@@ -483,7 +483,7 @@ We assume that module identifiers coincide with file names."
(proof-shell-config-done))
-(defun lego-pbp-mode-config ()
+(defun lego-goals-mode-config ()
(setq pbp-change-goal "Next %s;"
pbp-error-regexp lego-error-regexp)
(setq font-lock-keywords lego-font-lock-terms)