aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-depends.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-07 10:08:59 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-07 10:08:59 +0000
commite2ac74a6bcca223394d2db5399394ef0fd445c77 (patch)
tree4ac21126179a94ec28f28c5d5fc7428a547f076d /generic/proof-depends.el
parent4d0382787b8549521e49b471a5ffc1ffdb0b43ff (diff)
Add require, fix menu capitalization.
Diffstat (limited to 'generic/proof-depends.el')
-rw-r--r--generic/proof-depends.el12
1 files changed, 7 insertions, 5 deletions
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 07e74774..2c421d4e 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -12,6 +12,8 @@
;; within proofs. Code rewritten by David Aspinall.
;;
+(require 'span)
+
;; Variables
(defvar proof-thm-names-of-files nil
@@ -117,23 +119,23 @@ proof-last-theorem-dependencies is set."
"Make a portion of a context-sensitive menu showing proof dependencies."
(list
"-------------"
- (proof-dep-make-submenu "Local dependency..."
+ (proof-dep-make-submenu "Local Dependency..."
(lambda (namespan) (car namespan))
'proof-goto-dependency
(span-property span 'dependencies-within-file))
- (proof-make-highlight-depts-menu "Highlight dependencies"
+ (proof-make-highlight-depts-menu "Highlight Dependencies"
'proof-highlight-depcs
span 'dependencies-within-file)
- (proof-dep-make-submenu "Local dependents..."
+ (proof-dep-make-submenu "Local Dependents..."
(lambda (namepos) (car namepos))
'proof-goto-dependency
(span-property span 'dependents))
- (proof-make-highlight-depts-menu "Highlight dependents"
+ (proof-make-highlight-depts-menu "Highlight Dependents"
'proof-highlight-depts
span 'dependents)
["Unhighlight all" proof-dep-unhighlight t]
"-------------"
- (proof-dep-make-submenu "All dependencies..."
+ (proof-dep-make-submenu "All Dependencies..."
(lambda (name) (car name))
'proof-show-dependency
(mapcar 'list (span-property span 'dependencies)))))