diff options
author | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2009-09-01 09:38:18 +0000 |
---|---|---|
committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2009-09-01 09:38:18 +0000 |
commit | cd812062ae30b076da7720301428e69847a7b579 (patch) | |
tree | 11e464e4a614a8acb0485d113f26f9b8b3619985 /generic | |
parent | f73b31e26145063226949b4cee279bf97ed4c35d (diff) |
Fixed a parenthesis bug in pg-pbrpml.el + compatibility with 3.7 where proof-mode-for-script seems undefined
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-pbrpm.el | 8 |
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. |