diff options
author | 2002-09-11 14:47:58 +0000 | |
---|---|---|
committer | 2002-09-11 14:47:58 +0000 | |
commit | 44defeb4542decede229133132539af2e33a6adc (patch) | |
tree | 6abb4ad0dff4987077b5b7ed295b631e95c5bbd7 /coq | |
parent | 0d3342242b9a327331da0f71e667a0afe206430b (diff) |
Check on context menu doesn't seem useful.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 12 |
1 files changed, 9 insertions, 3 deletions
@@ -816,16 +816,22 @@ mouse activation." ;; Context-senstive in-span menu additions ;; +;; da: message to Pierre: I just put these in as examples, +;; maybe you can suggest some better commands to use on +;; `thm'. (Check maybe not much use since appears before +;; in the buffer anyway) (defun coq-create-span-menu (span idiom name) (if (string-equal idiom "proof") (let ((thm (span-property span 'name))) - (list (vector + (list ;(vector + ; "Check" + ; `(proof-shell-invisible-command + ; ,(format "Check %s." thm))) + (vector "Print Proof" `(proof-shell-invisible-command ,(format "Print Proof %s." thm))))))) - - ;;; Local Variables: *** ;;; tab-width:2 *** ;;; indent-tabs-mode:nil *** |