Span menu entry for proof using annotation + doc.

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