diff options
author | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2009-09-01 08:28:30 +0000 |
---|---|---|
committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2009-09-01 08:28:30 +0000 |
commit | 802687cdbfaadc37d0c9682177ffc0597266e94c (patch) | |
tree | b1888977fe608a62fb3d26386eb37b33a3dd2fa0 /phox/phox-pbrpm.el | |
parent | ef3def4933bdf3da95b10b6e154ca618bff4635f (diff) |
Removed support for x-symbol (I do not like it because it changes the buffer content !)
sym-lock is still available on xemacs only
various other bug fix.
Diffstat (limited to 'phox/phox-pbrpm.el')
-rw-r--r-- | phox/phox-pbrpm.el | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index fe202166..9c7411f3 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -211,12 +211,24 @@ (phox-lang-instance (nth 2 click-infos)) (nth 2 (car region-infos))) (concat - goal-prefix "instance " (nth 2 click-infos) " " - (nth 2 (car region-infos)) - ". ")))))) + (nth 2 (car region-infos)))))))) + + (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??) + (not region-infos)) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list 0 (concat + (phox-lang-open-instance (nth 2 click-infos))) + (concat + "instance " + (nth 2 click-infos) + " ") + (lambda (cmd spans) + (let ((span (pop spans))) + (concat cmd " " (span-string span))))))))) ; is clicking on a token with no selection (if (and (not region-infos) (not (string= (nth 2 click-infos) ""))) @@ -241,8 +253,7 @@ "unfold -ortho " (concat "unfold_hyp " (nth 1 click-infos) " -ortho ")) "$" - (nth 2 click-infos) - ". "))))) + (nth 2 click-infos)))))) (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??)) (let ((r (proof-shell-invisible-cmd-get-result (concat "is_locked " (nth 2 click-infos))))) @@ -253,16 +264,14 @@ (concat goal-prefix "unlock " - (nth 2 click-infos) - ". "))))) + (nth 2 click-infos)))))) (setq pbrpm-rules-list (append pbrpm-rules-list (list (list 0 (phox-lang-lock (nth 2 click-infos)) (concat goal-prefix "lock " - (nth 2 click-infos) - ". "))))))))))) + (nth 2 click-infos)))))))))))) (let ((arg (if (and region-infos (not (cdr region-infos))) (nth 2 (car region-infos)) " "))) (setq pbrpm-rules-list |