diff options
| -rw-r--r-- | generic/proof-config.el | 26 | ||||
| -rw-r--r-- | generic/proof-script.el | 5 | ||||
| -rw-r--r-- | isa/isa.el | 5 |
3 files changed, 8 insertions, 28 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 0af8af7e..a1e815a0 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -193,7 +193,8 @@ deleted automatically.") :bold t)) (t (:italic t :bold t))) - "*Face for declaration names in proof scripts." + "*Face for declaration names in proof scripts. +Exactly what uses this face depends on the proof assistant." :group 'proof-faces) (defconst proof-declaration-name-face 'proof-declaration-name-face @@ -208,7 +209,8 @@ both XEmacs 20.4 and Emacs 20.2's version of font-lock.") (:foreground "orchid")) (t (bold t))) - "*Face for names of tacticals in proof scripts." + "*Face for names of tacticals in proof scripts. +Exactly what uses this face depends on the proof assistant." :group 'proof-faces) (defconst proof-tacticals-name-face 'proof-tacticals-name-face @@ -370,14 +372,6 @@ insert when called interactively." :group 'prover-config) -;; FIXME: allow this to be set in the mode fn instead. -(defcustom proof-tags-support t - "If non-nil, include tags functions in menus. -This variable should be set before requiring proof.el" - :type 'boolean - :group 'prover-config) - - ;; ;; 4. Configuration for proof script mode @@ -828,16 +822,12 @@ data triggered by `proof-shell-retract-files-regexp'." :type 'string :group 'proof-general-internals) -;; FIXME: da: could we put these into another keymap already? -;; FIXME: da: it's offensive to experienced users to rebind global stuff -;; like meta-tab, this should be removed. + +;; FIXME: da: could we put these into another keymap shared across the +;; various PG modes? (defcustom proof-universal-keys - (append - '(([(control c) (control c)] . proof-interrupt-process) + '(([(control c) (control c)] . proof-interrupt-process) ([(control c) (control v)] . proof-execute-minibuffer-cmd)) - (if proof-tags-support - '(([(meta tab)] . tag-complete-symbol)) - nil)) "List of keybindings which for the script and response buffer. Elements of the list are tuples (k . f) where `k' is a keybinding (vector) and `f' the designated function." diff --git a/generic/proof-script.el b/generic/proof-script.el index 8e92e200..5de35455 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1397,11 +1397,6 @@ No action if BUF is nil." :active (proof-shell-live-buffer)] ["Exit proof assistant" proof-menu-exit :active (proof-shell-live-buffer)]) - (if proof-tags-support - (list - "----" - ["Find definition/declaration" find-tag-other-window t]) - nil) (list proof-help-menu) (list proof-buffer-menu)) "Proof General menu for various modes.") @@ -9,11 +9,6 @@ ;; - - -;; FIXME: this most be done before loading proof-config, shame. -(setq proof-tags-support nil) ; we don't want it, no isatags prog. - ;; Add Isabelle image onto splash screen (customize-set-variable 'proof-splash-extensions |