diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 09:57:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 09:57:12 +0000 |
| commit | f810ee2ebc41844c07458888a0030dcf5122a988 (patch) | |
| tree | 0abd2c724cb12eabb05a7d5473d3f022417356a4 /generic/proof-depends.el | |
| parent | 0d884890e6c75cf93e3f647bf40d399345088c71 (diff) | |
Fix autoload for context menu; add proof-shell-show-dependency-cmd.
Diffstat (limited to 'generic/proof-depends.el')
| -rw-r--r-- | generic/proof-depends.el | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 2c421d4e..22faaa83 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -115,8 +115,10 @@ proof-last-theorem-dependencies is set." ;; which the dependency information is used. +;;;###autoload (defun proof-dependency-in-span-context-menu (span) "Make a portion of a context-sensitive menu showing proof dependencies." + ;; FIXME: might only activate this for dependency-relevant spans. (list "-------------" (proof-dep-make-submenu "Local Dependency..." @@ -168,8 +170,9 @@ If LIST is empty, return a disabled menu item with NAME." (skip-chars-forward " \t\n")) (defun proof-show-dependency (thm) - ;; FIXME: make this prover independent with new regexp for print command!! - (proof-shell-invisible-command (format "thm \"%s\";" thm))) + "Show dependency THM using `proof-show-dependency-cmd'." + (if proof-shell-show-dependency-cmd ;; robustness + (proof-shell-invisible-command (format proof-shell-show-dependency-cmd thm)))) (defun proof-highlight-depcs (name nmspans) (let ((helpmsg (concat "This item is a dependency (ancestor) of " name))) |