aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-pbrpm.el
diff options
context:
space:
mode:
authorGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2009-09-01 09:38:18 +0000
committerGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2009-09-01 09:38:18 +0000
commitcd812062ae30b076da7720301428e69847a7b579 (patch)
tree11e464e4a614a8acb0485d113f26f9b8b3619985 /generic/pg-pbrpm.el
parentf73b31e26145063226949b4cee279bf97ed4c35d (diff)
Fixed a parenthesis bug in pg-pbrpml.el + compatibility with 3.7 where proof-mode-for-script seems undefined
Diffstat (limited to 'generic/pg-pbrpm.el')
-rw-r--r--generic/pg-pbrpm.el8
1 files changed, 5 insertions, 3 deletions
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 2138de08..3fc5916c 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -93,7 +93,9 @@ Matches the region to be returned.")
; needs to be fixed here, the mode could be some other prover
; (phox-mode)
; da: proof-mode-for-script should do it
- (funcall 'proof-mode-for-script)
+; cr: proof-mode-for-script is not defined in 3.7
+ (if (functionp 'proof-mode-for-script)
+ (funcall 'proof-mode-for-shell) (funcall 'proof-mode))
(add-hook 'after-change-functions 'pg-pbrpm-menu-change-hook nil t)
(pg-pbrpm-erase-buffer-menu)))
(set-buffer pg-pbrpm-buffer-menu))
@@ -238,7 +240,7 @@ The prover command is processed via pg-pbrpm-run-command."
;; buffer with font lock on.
(mapc 'span-read-only pg-pbrpm-spans)
(make-dialog-frame '(width 80 height 30)))
- (beep)))))
+ (beep))))))
(defun pg-pbrpm-setup-span (start end)
"Set up the span in the menu buffer."
@@ -298,7 +300,7 @@ The prover command is processed via pg-pbrpm-run-command."
(setq start (if pos pos end)))))
(cons allspan (sort (reverse spans) (lambda (sp1 sp2)
(< (span-property sp1 'goalnum)
- (span-property sp1 'goalnum)))))))))
+ (span-property sp1 'goalnum))))))))
(defun pg-pbrpm-run-command (args)
"Insert COMMAND into the proof queue and then run it.