In a fit of autocracy, removed proof-tags-support, binding for

M-tab and appearance of Find Tags in PG menu.  The menu entry
already appears in Tools->Tags, and users should bind M-tab for
themselves.

2 files changed, 8 insertions, 23 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.")