diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-08-14 21:17:57 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-08-14 21:17:57 +0000 |
commit | ef60a74b43d0216d8aaa1d79c3c6ead0ba3378cf (patch) | |
tree | 5ad7143d809a45197590db7140fedfc893c18386 /isa | |
parent | a0466897230202bff4724a9c91b037ea0862d817 (diff) |
Added Fiona's changes.
Diffstat (limited to 'isa')
-rw-r--r-- | isa/thy-mode.el | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/isa/thy-mode.el b/isa/thy-mode.el index a5663ad4..02785018 100644 --- a/isa/thy-mode.el +++ b/isa/thy-mode.el @@ -1,4 +1,4 @@ -;; isa-thy-mode.el - Mode for Isabelle theory files. +;; thy-mode.el - Mode for Isabelle theory files. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> ;; Maintainer: Isabelle maintainer <isabelle@dcs.ed.ac.uk> @@ -171,7 +171,7 @@ You can use the following format characters: (define-key map "\C-k" 'thy-kill-line) (setq thy-mode-map map))) -(defun thy-add-menus () +(defun thy-add-menus (&optional file) "Add Proof General and Isabelle menu to current menu bar." (require 'proof-script) ; Later: proof-menu, autoloaded (easy-menu-define thy-mode-pg-menu @@ -210,8 +210,13 @@ You can use the following format characters: :active (proof-locked-region-full-p)] ["Next error" proof-next-error t] ["Switch to script" thy-find-other-file t]))) - (easy-menu-add thy-mode-pg-menu thy-mode-map) - (easy-menu-add thy-mode-isa-menu thy-mode-map)) + (easy-menu-add thy-mode-pg-menu thy-mode-map) + (easy-menu-add thy-mode-isa-menu thy-mode-map) + + (if file + (progn (easy-menu-remove thy-mode-deps-menu) + (thy-menu-define-deps file) + (easy-menu-add thy-mode-deps-menu thy-mode-map)))) (defun thy-mode (&optional nomessage) |