aboutsummaryrefslogtreecommitdiffhomepage
path: root/plastic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 13:48:32 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 13:48:32 +0000
commitc9131112526984c135c29e0b3dd465642e05d5fd (patch)
tree42362af9758625c0f36f317156251065992f2a8a /plastic
parent8194bdb86647cc5f2462deee358938bf676231d6 (diff)
pbp-mode -> goals-mode
Diffstat (limited to 'plastic')
-rw-r--r--plastic/plastic.el10
1 files changed, 5 insertions, 5 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el
index a4b0bf51..4d15bf05 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -212,9 +212,9 @@
(plastic-init-syntax-table)
(proof-response-config-done)))
-(define-derived-mode plastic-pbp-mode pbp-mode
+(define-derived-mode plastic-goals-mode proof-goals-mode
"PlasticGoals" "Plastic Goal State"
- (plastic-pbp-mode-config))
+ (plastic-goals-mode-config))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -367,9 +367,9 @@ Given is the first SPAN which needs to be undone."
(defun plastic-pre-shell-start ()
(setq proof-prog-name (concat plastic-prog-name "")
;; set cmd-line flag
- proof-mode-for-shell 'plastic-shell-mode
+ proof-mode-for-shell 'plastic-shell-mode
proof-mode-for-response 'plastic-response-mode
- proof-mode-for-pbp 'plastic-pbp-mode)
+ proof-mode-for-goals 'plastic-goals-mode)
(setenv "PROOF_GENERAL" "") ;; signal to plastic, use annotations
)
@@ -571,7 +571,7 @@ We assume that module identifiers coincide with file names."
(proof-shell-config-done)
)
-(defun plastic-pbp-mode-config ()
+(defun plastic-goals-mode-config ()
(setq pbp-change-goal "Next %s;"
pbp-error-regexp plastic-error-regexp)
(setq font-lock-keywords plastic-font-lock-terms)