path: root/generic/proof-menu.el

;; proof-menu.el  Menu and keymaps for Proof General
;;
;; Copyright (C) 2000 LFCS Edinburgh. 
;; Authors:  David Aspinall
;;
;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
;;
;; $Id$
;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Key bindings
;;;

;;;###autoload
(defun proof-menu-define-keys (map)
(define-key map [(control c) a] (proof-assistant-keymap))
(define-key map [(control c) (control a)] 'proof-goto-command-start)
(define-key map [(control c) (control b)] 'proof-process-buffer)
; C-c C-c is proof-interrupt-process in universal-keys
(define-key map [(control c) (control e)] 'proof-goto-command-end)
(define-key map [(control c) (control n)] 'proof-assert-next-command-interactive)
(define-key map [(control c) (control p)] 'proof-prf)
(define-key map [(control c) (control r)] 'proof-retract-buffer)
(define-key map [(control c) (control s)] 'proof-toggle-active-scripting)
(define-key map [(control c) (control t)] 'proof-ctxt)
(define-key map [(control c) (control u)] 'proof-undo-last-successful-command)
(define-key map [(control c) (control backspace)] 'proof-undo-and-delete-last-successful-command)
; C-c C-v is proof-minibuffer-cmd in universal-keys
(define-key map [(control c) (control z)] 'proof-frob-locked-end)
(define-key map [(control c) (control ?.)] 'proof-goto-end-of-locked)
(define-key map [(control c) (control return)] 'proof-goto-point)
(cond ((string-match "XEmacs" emacs-version)
(define-key map [(control button3)]	  'proof-mouse-goto-point)
(define-key map [(control button1)]	  'proof-mouse-track-insert)) ; no FSF
      (t 
(define-key map [mouse-3]		  'proof-mouse-goto-point))) ; FSF
;; NB: next binding overwrites comint-find-source-code.  
(define-key map [(control c) (control f)] 'proof-find-theorems)
(define-key map [(control c) (control h)] 'proof-help)
;; FIXME: not implemented yet 
;; (define-key map [(meta p)]		  'proof-previous-matching-command)
;; (define-key map [(meta n)]		  'proof-next-matching-command)
;; Deprecated bindings
;(define-key map [(control c) return] 'proof-assert-next-command)
;(define-key map [(control c) ?u] 'proof-retract-until-point-interactive)
;; Add the universal keys bound in all PG buffers.
(proof-define-keys map proof-universal-keys))







;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Functions to define the menus
;;;

;; The main Proof-General generic menu

;;;###autoload
(defun proof-menu-define-main ()
  (easy-menu-define 
   proof-mode-menu  
   proof-mode-map
   "The main Proof General menu"
   (cons proof-general-name
	 (append
	  proof-toolbar-scripting-menu
	  proof-menu
	  (list "----")
	  (append
	   (list (customize-menu-create 'proof-general))
	   (list (customize-menu-create 'proof-general-internals 
					"Internals")))
	  proof-bug-report-menu))))


;; The proof assistant specific menu

;;;###autoload
(defun proof-menu-define-specific ()
  (easy-menu-define 
   proof-assistant-menu 
   proof-mode-map
   (concat "The menu for " proof-assistant)
   (cons proof-assistant
	 (append
	  (proof-assistant-menu-entries)
	  '("----")
	  (proof-assistant-favourites)
	  '(["Add favourite" 
	     (call-interactively 'proof-add-favourite) t])
	  '("----")
	  (list
	   (cons "Help"
		 (append 
		  `(;; FIXME: should only put these two on the
		    ;; menu if the settings are non-nil.
		    [,(concat proof-assistant " information")
		     (proof-help) t]
		    [,(concat proof-assistant " web page")
		     (browse-url proof-assistant-home-page) t])
		  (proof-ass help-menu-entries))))))))
    

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Contents of the generic menus
;;;


(defun proof-deftoggle-fn (var &optional othername)
  "Define a function <VAR>-toggle for toggling a boolean customize setting VAR.
The toggle function uses customize-set-variable to change the variable.
OTHERNAME gives an alternative name than the default <VAR>-toggle."
  (eval
   `(defun ,(if othername othername 
	      (intern (concat (symbol-name var) "-toggle"))) (arg)
	      ,(concat "Toggle `" (symbol-name var) "'. With ARG, turn on iff ARG>0.
This function simply uses customize-set-variable to set the variable.
It was constructed with `proof-customize-toggle-fn'.")
	      (interactive "P")
	      (customize-set-variable 
	       (quote ,var)
	       (if (null arg) (not ,var)
		 (> (prefix-numeric-value arg) 0))))))

;;;###autoload
(defmacro proof-deftoggle (var &optional othername)
  "Define a function VAR-toggle for toggling a boolean customize setting VAR.
VAR, OTHERNAME are not evaluated.  
The function is defined with `proof-customize-toggle-fn', which see."
  `(proof-deftoggle-fn (quote ,var) (quote ,othername)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Contents of the generic menus
;;;

(defvar proof-help-menu
  '("Help"
    ["Proof General home page"
     (browse-url proof-general-home-page) t]
    ["Proof General Info"
     (info "ProofGeneral") t])
  "Proof General help menu.")

(defvar proof-buffer-menu
  '("Buffers"
    ["Active scripting"
     (proof-switch-to-buffer proof-script-buffer)
     :active (buffer-live-p proof-script-buffer)]
    ["Goals"
     (proof-switch-to-buffer proof-goals-buffer t)
     :active (buffer-live-p proof-goals-buffer)]
    ["Response"
     (proof-switch-to-buffer proof-response-buffer t)
     :active (buffer-live-p proof-response-buffer)]
    ["Shell"
     (proof-switch-to-buffer proof-shell-buffer)
     :active (buffer-live-p proof-shell-buffer)])
  "Proof General buffer menu.")

;; Make the togglers used in options menu below

(proof-deftoggle proof-dont-switch-windows)
(proof-deftoggle proof-delete-empty-windows)
(proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle)
(proof-deftoggle proof-output-fontify-enable proof-output-fontify-toggle)
(proof-deftoggle proof-x-symbol-enable proof-x-symbol-toggle)

(defvar proof-quick-opts-menu
  `("Options"
    ["Don't switch windows" proof-dont-switch-windows-toggle
     :style toggle
     :selected proof-dont-switch-windows]
    ["Delete empty windows" proof-delete-empty-windows-toggle
     :style toggle
     :selected proof-delete-empty-windows]
    ["Multiple frames" proof-multiple-frames-toggle
     :style toggle
     :selected proof-multiple-frames-enable]
    ["Output highlighting" proof-output-fontify-toggle
     :active t
     :style toggle
     :selected proof-output-fontify-enable]
    ["Toolbar" proof-toolbar-toggle
     :active (and (featurep 'toolbar) 
		  (boundp 'proof-buffer-type)
		  (eq proof-buffer-type 'script))
     :style toggle
     :selected proof-toolbar-enable]
    ["X-Symbol" proof-x-symbol-toggle
     :active (proof-x-symbol-support-maybe-available)
     :style toggle
     :selected proof-x-symbol-enable]
    ("Follow mode" 
     ["Follow locked region" 
      (customize-set-variable 'proof-follow-mode 'locked)
     :style radio
     :selected (eq proof-follow-mode 'locked)]
     ["Keep locked region displayed" 
      (customize-set-variable 'proof-follow-mode 'follow)
     :style radio
     :selected (eq proof-follow-mode 'follow)]
     ["Never move" 
      (customize-set-variable 'proof-follow-mode 'ignore)
     :style radio
     :selected (eq proof-follow-mode 'ignore)]))
  "Proof General quick options.")

(defvar proof-shared-menu
  (append
   ;; FIXME: should we move the start and stop items to 
   ;; the specific menu?  
   ;; (They only seem specific because they mention the PA).
    (list
     (vector
      (concat "Start " proof-assistant)
      'proof-shell-start
      ':active '(not (proof-shell-live-buffer)))
     (vector
      (concat "Exit " proof-assistant)
      'proof-shell-exit
      ':active '(proof-shell-live-buffer)))
    (list proof-buffer-menu)
    (list proof-quick-opts-menu)
    (list proof-help-menu))
  "Proof General menu for various modes.")

(defvar proof-bug-report-menu
  (list "----"
   ["About Proof General" proof-splash-display-screen]
   ["Submit bug report"   proof-submit-bug-report])
  "Proof General menu for submitting bug report (one item plus separator).")

(defvar proof-menu  
  (append '("----"
	    ["Scripting active" proof-toggle-active-scripting
	     :style toggle
	     :selected (eq proof-script-buffer (current-buffer))]
	    ["Electric terminator" proof-electric-terminator-toggle
	     :style toggle
             :selected proof-electric-terminator-enable]
	    ["Function menu" function-menu
	     :active (fboundp 'function-menu)]
	    "----")
          proof-shared-menu)
  "The Proof General generic menu.")



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Favourites mechanism for specific menu
;;;


(defmacro proof-defshortcut (fn string &optional key)
  "Define shortcut function FN to insert STRING, optional keydef KEY.
This is intended for defining proof assistant specific functions.
STRING is inserted using `proof-insert', which see.
KEY is added onto proof-assistant map."
  (if key
      (eval
       `(define-key (proof-ass keymap) ,key (quote ,fn))))
  `(defun ,fn ()
     (concat "Shortcut command to insert " ,string " into the current buffer.")
     (interactive)
     (proof-insert ,string)))

(defmacro proof-definvisible (fn string &optional key)
  "Define function FN to send STRING to proof assistant, optional keydef KEY.
This is intended for defining proof assistant specific functions.
STRING is sent using proof-shell-invisible-command, which see.
KEY is added onto proof-assistant map."
  (if key
      (eval
       `(define-key (proof-ass keymap) ,key (quote ,fn))))
  `(defun ,fn ()
     (concat "Command to send " ,string " to the proof assistant.")
     (interactive)
     (proof-shell-invisible-command ,string)))


;;; Code for adding "favourites" to the proof-assistant specific menu

(defvar proof-make-favourite-cmd-history nil
  "History for proof-make-favourite.")

(defun proof-add-favourite (command inscript menuname &optional key)
  "Define and add a \"favourite\" proof-assisant function to the menu bar.
The favourite function will issue COMMAND to the proof assistant.  
COMMAND is inserted into script (not sent immediately) if INSCRIPT non-nil.
MENUNAME is the name of the function for the menu.
KEY is the optional key binding
This function defines a function and returns a menu entry 
suitable for adding to the proof assistant menu."
  (interactive 
   (list
    (read-string (concat "Command to send to " proof-assistant ": ") nil 
		 proof-make-favourite-cmd-history)
    (y-or-n-p "Should command be recorded in script? ")
    (read-string "Name of command on menu: ")
    (if (y-or-n-p "Set a keybinding for this command? : ")
	(read-key-sequence "Type the key to use (I recommend C-c a <key>): " nil t))))
  (let* ((menunames	(split-string (downcase menuname)))
	 (menuname-sym  (proof-sym (proof-splice-separator "-" menunames)))
	 (menu-fn	menuname-sym) (i 1))
    (while (fboundp menu-fn)
      (setq menu-fn (intern (concat (symbol-name menuname-sym)
				    "-" (int-to-string i))))
      (incf i))
    (if inscript
	`(proof-defshortcut ,menu-fn ,command ,key)
      `(proof-definvisible ,menu-fn ,command ,key))
    (let ((menu-entry (vector menuname menu-fn t)))
      (customize-save-variable 'proof-assistant-menu-entries
			       (append proof-assistant-menu-entries 
				       (list menu-entry)))
      ;; Unfortunately, (easy-menu-add-item proof-assistant-menu nil ..)
      ;; seems buggy, it adds to main menu. But with "Coq" argument 
      ;; for path it adds a submenu!   The item argument seems to be
      ;; something special, but no way to make an item for adding
      ;; an ordinary item?!
      (easy-menu-add-item proof-assistant-menu 
			  '("Favourites")
			  menu-entry 
			  "Add favourite"))))



(provide 'proof-menu)
;; proof-menu.el ends here.