diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-16 17:22:01 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-16 17:22:01 +0000 |
| commit | a61b77aad2a2902cc8d6d191d5b75615873db930 (patch) | |
| tree | 5ff297bb325ac9063199fbbac7fc24969d35eabc /isar | |
| parent | 555f39491e50772caacae0b9dbd276846befa361 (diff) | |
Use shared span menu
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 15 |
1 files changed, 1 insertions, 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 () @@ -605,19 +605,6 @@ proof-shell-retract-files-regexp." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;; 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") ;; |