Added buffers menu, and added shared menu to shell and response buffers.

2 files changed, 67 insertions, 19 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index c393855e..e242eda4 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -72,14 +72,6 @@ However, fume-func's version is incorrect"
       (and (re-search-forward r nil t)
 	   (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))
 
-;; append-element in tl-list
-(defun proof-append-element (ls elt)
-  "Append ELT to last of LS if ELT is not nil. [proof.el]
-This function coincides with `append-element' in the package
-[tl-list.el.]"
-  (if elt
-      (append ls (list elt))
-    ls))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1288,6 +1280,19 @@ Start up the proof assistant if necessary."
   (interactive)
   (info "ProofGeneral"))
 
+;; A handy utility function used in buffer menu.
+(defun proof-switch-to-buffer (buf &optional noselect)
+  "Switch to or display buffer BUF in other window unless already displayed.
+If optional arg NOSELECT is true, don't switch, only display it.
+No action if BUF is nil."
+  ;; Maybe this needs to be more sophisticated, using 
+  ;; proof-display-and-keep-buffer ?
+  (and buf
+       (unless (eq buf (window-buffer (selected-window)))
+	 (if noselect
+	     (display-buffer buf t)
+	   (switch-to-buffer-other-window buf)))))
+
 (defun proof-menu-exit ()
   "Exit Proof-assistant."
   (interactive)
@@ -1301,11 +1306,23 @@ Start up the proof assistant if necessary."
      (browse-url proof-proof-general-home-page) t]
     ["Proof General Info" proof-menu-invoke-info t]
     )
-  "The Help Menu in Script Management.")
+  "Proof General help menu.")
+
+(defvar proof-buffer-menu
+  '("Buffers"
+    ["Active scripting"
+     (proof-switch-to-buffer (car-safe proof-script-buffer-list))
+     :active (car-safe proof-script-buffer-list)]
+    ["Response"
+     (proof-switch-to-buffer proof-response-buffer t)
+     :active proof-response-buffer]
+    ["Shell"
+     (proof-switch-to-buffer proof-shell-buffer)
+     :active (proof-shell-live-buffer)])
+  "Proof General buffer menu.")
 
 (defvar proof-shared-menu
-  (proof-append-element
-   (append
+  (append
     (list
      ["Display context" proof-ctxt
       :active (proof-shell-live-buffer)]
@@ -1317,8 +1334,10 @@ Start up the proof assistant if necessary."
 	(list
 	 "----"
 	 ["Find definition/declaration" find-tag-other-window t])
-      nil))
-    proof-help-menu))
+      nil)
+    (list proof-help-menu)
+    (list proof-buffer-menu))
+  "Proof General menu for various modes.")
 
 (defvar proof-menu  
   (append '("Commands"
@@ -1332,10 +1351,8 @@ Start up the proof assistant if necessary."
 		    "--:doubleLine" "----"))
           proof-shared-menu
           )
-  "*The menu for the proof assistant.")
+  "The menu for the proof assistant.")
 
-(defvar proof-shell-menu proof-shared-menu
-  "The menu for the Proof-assistant shell")
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index b4a5182f..7354d3df 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -9,7 +9,10 @@
 ;; $Id$
 ;;
 
-(require 'proof)
+;; FIXME: needed because of menu definitions, which should
+;; be factored out into proof-menus.  Then require here is
+;; just on proof-shell.
+(require 'proof-script)			
 
 ;; Nuke some byte compiler warnings.
 
@@ -38,6 +41,10 @@
 	    proof-register-possibly-new-processed-file
 	    proof-restart-buffers)))
 
+;; FIXME:
+;; Some variables from proof-shell are also used, in particular,
+;; the menus.  These should probably be moved out to proof-menu.
+
 ;;
 ;; Internal variables used by shell mode
 ;;
@@ -992,14 +999,25 @@ Annotations are characters 128-255."
   (setq proof-re-term-or-comment 
 	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
 		"\\|" (regexp-quote proof-comment-end)))
+  
+  ;; easy-menu-add must be in the mode function for XEmacs.
+  (easy-menu-add proof-shell-mode-menu proof-shell-mode-map)
   ))
 
+;; watch difference with proof-shell-menu, proof-shell-mode-menu.
+(defvar proof-shell-menu proof-shared-menu
+  "The menu for the Proof-assistant shell")
 
-(easy-menu-define proof-shell-menu
+(easy-menu-define proof-shell-mode-menu
 		  proof-shell-mode-map
 		  "Menu used in Proof General shell mode."
 		  (cons proof-mode-name (cdr proof-shell-menu)))
 
+
+
+
+
+
 (defun proof-font-lock-minor-mode ()
   "Start font-lock as a minor mode in the current buffer."
 
@@ -1067,7 +1085,20 @@ Annotations are characters 128-255."
 (eval-and-compile
 (define-derived-mode proof-response-mode proof-universal-keys-only-mode
   "PGResp" "Responses from Proof Assistant"
-  (setq proof-buffer-type 'response)))
+  (setq proof-buffer-type 'response)
+  (easy-menu-add proof-response-mode-menu proof-response-mode-map)))
+
+
+(easy-menu-define proof-response-mode-menu
+		  proof-response-mode-map
+		  "Menu for Proof General response buffer."
+		  (cons proof-mode-name
+			(cdr proof-shared-menu)))
+
+
+			
+
+