diff options
| -rw-r--r-- | generic/proof-autoloads.el | 5 | ||||
| -rw-r--r-- | generic/proof-depends.el | 7 |
2 files changed, 9 insertions, 3 deletions
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index b76b9b52..ab02df2b 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -7,13 +7,16 @@ ;;;*** -;;;### (autoloads (proof-depends-process-dependencies) "proof-depends" "generic/proof-depends.el") +;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies) "proof-depends" "generic/proof-depends.el") (autoload 'proof-depends-process-dependencies "proof-depends" "\ Process dependencies reported by prover, for NAME in span GSPAN. Called from `proof-done-advancing' when a save is processed and proof-last-theorem-dependencies is set." nil nil) +(autoload 'proof-dependency-in-span-context-menu "proof-depends" "\ +Make a portion of a context-sensitive menu showing proof dependencies." nil nil) + ;;;*** ;;;### (autoloads (proof-easy-config) "proof-easy-config" "generic/proof-easy-config.el") 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))) |