From a61b77aad2a2902cc8d6d191d5b75615873db930 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 16 Aug 2002 17:22:01 +0000
Subject: Use shared span menu

---
 isar/isar.el | 15 +--------------
 1 file changed, 1 insertion(+), 14 deletions(-)

diff --git a/isar/isar.el b/isar/isar.el
index f0ccf6b4..d0b8c6ec 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -169,7 +169,7 @@ See -k option for Isabelle interface script."
    proof-state-preserving-p     'isar-state-preserving-p
    proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list
    ;; span menu 
-   proof-script-span-context-menu-extensions 'isar-create-span-menu))
+   proof-script-span-context-menu-extensions 'isabelle-create-span-menu))
 
 
 (defun isar-shell-mode-config-set-variables ()
@@ -603,19 +603,6 @@ proof-shell-retract-files-regexp."
  (isar-markup-ml "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\",\"symbols\"]))"))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Span menu additions for Isar
-;;
-
-(defun isar-create-span-menu (span idiom name)
-  (if (string-equal idiom "proof")
-      (list (vector 
-	     "Visualise dependencies" 
-	     `(proof-shell-invisible-command 
-	       ,(format "thm_deps %s;" 
-			(span-property span 'name)))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Theorem dependencies  (experimental, uses Isabelle "patch")
-- 
cgit v1.2.3