diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 12 | ||||
| -rw-r--r-- | generic/proof-depends.el | 50 |
2 files changed, 40 insertions, 22 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 41c5e9d7..c10c0ee0 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1760,7 +1760,17 @@ This hook is used within Proof General to refresh the toolbar." ;;;;;; (defcustom proof-dependencies-system-specific nil - "doc TODO" + "Set this variable to handle system specific dependency output. +This must be a function with 1 parameter: the goalsave span of +the theorem being saved." + :type '(repeat function) + :group 'proof-shell) + +(defcustom proof-dependency-menu-system-specific nil + "Hook for system specific menu items for dependency menu. +This must be a function taking one argument: the span one which +the secific menu must be added. It must return a lit with the +same type as `proof-dependency-in-span-context-menu' returns." :type '(repeat function) :group 'proof-shell) ;;;;; diff --git a/generic/proof-depends.el b/generic/proof-depends.el index c3de97f7..6651e277 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -121,7 +121,7 @@ Called from `proof-done-advancing' when a save is processed and (span-set-property gspan 'dependencies-within-file depspans) (setq proof-last-theorem-dependencies nil) - (funcall 'proof-dependencies-system-specific name gspan))) + (funcall proof-dependencies-system-specific gspan))) @@ -136,27 +136,35 @@ Called from `proof-done-advancing' when a save is processed and ;;;###autoload (defun proof-dependency-in-span-context-menu (span) - "Make some menu entries showing proof dependencies of SPAN." + "Make some menu entries showing proof dependencies of SPAN. +Use `proof-dependency-menu-system-specific' to build system +specific entries." ;; FIXME: might only activate this for dependency-relevant spans. - (list - "-------------" - (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-highlight-depcs - span 'dependencies-within-file) - (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-highlight-depts - span 'dependents) - ["Unhighlight all" proof-dep-unhighlight t] - "-------------" - (proof-dep-alldeps-menu span))) + (let ((defmenu + (list + "-------------" + (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-highlight-depcs + span 'dependencies-within-file) + (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-highlight-depts + span 'dependents) + ["Unhighlight all" proof-dep-unhighlight t] + "-------------" + (proof-dep-alldeps-menu span)))) + (if (not proof-dependency-menu-system-specific) + defmenu + (append + (funcall proof-dependency-menu-system-specific span) + defmenu)))) (defun proof-dep-alldeps-menu (span) (or (span-property span 'dependencies-menu) ;; cached value |