Add span menu for thm_deps

2 files changed, 18 insertions, 0 deletions

diff --git a/isa/isa.el b/isa/isa.el
index b2cc64a2..bec0003d 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -125,6 +125,9 @@ and script mode."
    proof-shell-inform-file-retracted-cmd 
    "ProofGeneral.inform_file_retracted \"%s\";"
 
+   ;; span menu 
+   proof-script-span-context-menu-extensions 'isabelle-create-span-menu
+
    ;; Parsing error messages.  Bit tricky to allow for
    ;; multitude of possible error formats Isabelle spits out.
    ;; Ideally we shouldn't bother parsing errors that appear
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 0c23d1b4..1262e786 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -433,6 +433,21 @@ the function `pg-remove-specials' can be used instead)."
     (replace-match "\374" nil t)))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Context-senstive in-span menu additions 
+;;
+
+(defun isabelle-create-span-menu (span idiom name)
+  (if (string-equal idiom "proof")
+      (let ((thm (span-property span 'name)))
+	(list (vector 
+	       "Visualise dependencies" 
+	       `(proof-shell-invisible-command 
+		 ,(format (if isa-running-isar 
+			      "thm_deps %s;" "thm_deps [%s];") thm))
+	       (not (string-equal thm proof-unnamed-theorem-name)))))))
+
 
 (provide 'isabelle-system)
 ;; End of isabelle-system.el