aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-09-29 16:12:51 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-09-29 16:12:51 +0000
commit8eccb1871f63583d3235b8e619629adfad40e2f9 (patch)
treede7d0c5ba7f7c8cae28d3371014e9985a61ae055
parent3e240faf5383f2d717535c3043537e1cf6587791 (diff)
Re-enabled proof-by-pointing for testing purposes only. Fixed a bug.
-rw-r--r--generic/proof-shell.el5
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3d4fe192..f9db16ce 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -459,7 +459,7 @@ Proof General with the proof assistant."
(let ((a 0) (l (length string)) ls)
(while (< a l)
(setq ls (cons (int-to-string
- (aref string a))
+ (char-to-int (aref string a)))
(cons " " ls)))
(incf a))
(apply 'concat (nreverse ls))))
@@ -1616,7 +1616,8 @@ before and after sending the command."
proof-general-name "Proof by Pointing"
;; defined-derived-mode pbp-mode initialises pbp-mode-map
(setq proof-buffer-type 'pbp)
- ;; (define-key pbp-mode-map [(button2)] 'pbp-button-action)
+ ;; FIXME da: this was disabled, re-enabled for testing only!!
+ (define-key pbp-mode-map [(button2)] 'pbp-button-action)
;; FIXME da: add a menu here?
(erase-buffer)))