path: root/generic/proof-menu.el

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

(require 'proof-toolbar)		; needed for proof-toolbar-scripting-menu

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Miscellaneous commands
;;;

(defun proof-display-some-buffers ()
  "Display the reponse or goals buffer, toggling between them.
If in three window or multiple frame mode, display both buffers."
  (interactive)
  (cond
   ((or proof-dont-switch-windows proof-multiple-frames-enable)
    ;; Display both
    (proof-switch-to-buffer proof-response-buffer 'noselect)
    (proof-switch-to-buffer proof-goals-buffer 'noselect))
   ((and (buffer-live-p proof-response-buffer)
	 (get-buffer-window proof-response-buffer 'visible))
    ;; Response buffer visible, let's display goals
    (proof-switch-to-buffer proof-goals-buffer 'noselect))
   (t
    ;; Response buffer invisible, let's display it
    (proof-switch-to-buffer proof-response-buffer 'noselect))))


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

;;;###autoload
(defun proof-menu-define-keys (map)
;; M-a and M-e are usually {forward,backward}-sentence.
;; Some modes also override these with similar commands
(define-key map [(meta a)] 'proof-forward-command)
(define-key map [(meta e)] 'proof-backward-command)
(define-key map [(control c) (control a)] (proof-ass keymap))
(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 f)] 'proof-find-theorems)
(define-key map [(control c) (control h)] 'proof-help)
(define-key map [(control c) (control l)] 'proof-display-some-buffers)
(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 z)] 'proof-frob-locked-end)
(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 ?.)] '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.  
;; FIXME: not implemented yet 
;; (define-key map [(meta p)]		  'proof-previous-matching-command)
;; (define-key map [(meta n)]		  'proof-next-matching-command)
;; Standard binding for completion
(define-key map [(control return)] 'proof-script-complete)
;; Add the universal keys bound in all PG buffers.
;; C-c ` is next-error in universal-keys
(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
	  proof-config-menu
	  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-ass menu-entries)
	  '("----")
	  (or proof-menu-favourites
	      (proof-menu-define-favourites-menu))
	  (or proof-menu-settings
	      (proof-menu-define-settings-menu))
	  '("----")
	  (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
	   (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
;;;

(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"
    ["Display some"
     proof-display-some-buffers
     :active (or (buffer-live-p proof-goals-buffer)
		 (buffer-live-p proof-response-buffer))]
    ["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-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)

(defvar proof-quick-opts-menu
  `("Options"
    ["Three window mode" 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-ass 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.")

(defconst proof-shared-menu
  (append
   (list "----")
   (list proof-buffer-menu)
   (list proof-quick-opts-menu)
   (list proof-help-menu))
  "Proof General menu for various modes.")

(defconst proof-config-menu
  (list 
   "----"
   (customize-menu-create 'proof-general)
   (customize-menu-create 'proof-general-internals 
			  "Internals"))
  "Proof General configuration menu.")

(defvar proof-bug-report-menu
  (list "----"
   ["About Proof General" proof-splash-display-screen t]
   ["Submit bug report"   proof-submit-bug-report t])
  "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)]
	    ["Complete identifier" complete t]
	    ["Next error" proof-next-error
	     :active proof-shell-next-error-regexp])
	    proof-shared-menu)
  "The Proof General generic menu.  Functions for scripting buffers.")


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

(defvar proof-menu-favourites nil
  "The Proof General favourites menu for the current proof assistant.")

(defun proof-menu-define-favourites-menu ()
  "Return menu generated from `PA-favourites'."
  (let ((favs (reverse (proof-ass favourites))) ents)
    (while favs
      (setq ents (cons (apply 'proof-def-favourite (car favs)) ents))
      (setq favs (cdr favs)))
    (setq proof-menu-favourites 
	  (list 
	   (cons "Favourites" 
		 (append ents
			 '(["Add favourite" 
			    (call-interactively 
			     'proof-add-favourite) t])))))))
  
;;; Define stuff from favourites

;;;###autoload
(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) (quote ,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) (quote ,key) (quote ,fn))))
  `(defun ,fn ()
     ;; FIXME: docstring broken! and above.
     (concat "Command to send " ,string " to the proof assistant.")
     (interactive)
     (proof-shell-invisible-command ,string)))

(defun proof-def-favourite (command inscript menuname &optional key new)
  "Define and a \"favourite\" proof assisant function.
See doc of `proof-add-favourite' for first four arguments.
Extra NEW flag means that this should be a new favourite, so check
that function defined is not already bound.
This function defines a function and returns a menu entry 
suitable for adding to the proof assistant menu."
  (let* ((menunames	(split-string (downcase menuname)))
	 (menuname-sym  (proof-sym (proof-splice-separator "-" menunames)))
	 (menu-fn	menuname-sym) (i 1))
    (while (and new (fboundp menu-fn))
      (setq menu-fn (intern (concat (symbol-name menuname-sym)
				    "-" (int-to-string i))))
      (incf i))
    (if inscript
	(eval `(proof-defshortcut ,menu-fn ,command ,key))
      (eval `(proof-definvisible ,menu-fn ,command ,key)))
    ;; Return menu entry
    (vector menuname menu-fn t)))


;;; 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."
  (interactive 
   (let* 
       ((cmd (read-string 
	      (concat "Command to send to " proof-assistant ": ") 
	      (buffer-substring
	       (save-excursion
		 (beginning-of-line-text)
		 (point))
	       (point))
	      proof-make-favourite-cmd-history))
	(ins (y-or-n-p "Should command be recorded in script? "))
	(men (read-string "Name of command on menu: " cmd))
	(key (if (y-or-n-p "Set a keybinding for this command? : ")
		 (events-to-keys
	          (read-key-sequence 
		   "Type the key to use (binding will be C-c C-a <key>): " nil t)))))
     (list cmd ins men key)))
  (let ((menu-entry (proof-def-favourite command inscript menuname key t)))
    ;; If definition succeeds, add to customize variable and save immediately.
    ;; FIXME: should maybe overwrite previous duplicates, use 
    ;; update rather than append.
    (customize-save-variable  (proof-ass-sym favourites)
			      (append (proof-ass favourites)
				      (list 
				       (list command inscript menuname key))))
    (easy-menu-add-item proof-assistant-menu 
			'("Favourites") menu-entry "Add favourite")))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Proof assistant settings mechanism.
;;;

(defvar proof-assistant-settings nil
 "A list of default values kept in Proof General for current proof assistant.
A list of lists (SYMBOL SETTING TYPE) where SETTING is a string value
to send to the proof assistant using the value of SYMBOL and 
and the function `proof-assistant-format'.  The TYPE item determines
the form of the menu entry for the setting.")

(defvar proof-menu-settings nil
  "Settings submenu for Proof General.")

(defun proof-menu-define-settings-menu ()
  "Return menu generated from `proof-assistant-settings'."
  (let ((setgs proof-assistant-settings) ents)
    (while setgs
      (setq ents (cons 
		  (apply 'proof-menu-entry-for-setting (car setgs)) ents))
      (setq setgs (cdr setgs)))
    (if ents
	(setq proof-menu-settings 
	      (list (cons "Settings" ents))))))

(defun proof-menu-entry-name (symbol)
  "Return a nice menu entry name for SYMBOL."
  (upcase-initials 
   (replace-in-string (symbol-name symbol) "-" " ")))

(defun proof-menu-entry-for-setting (symbol setting type)
  (let ((entry-name  (proof-menu-entry-name symbol))
	(pasym	     (proof-ass-symv symbol)))
    (cond
     ((eq type 'boolean)
      (vector entry-name 
	      (proof-deftoggle-fn pasym)
	      :style 'toggle
	      :selected pasym))
     ((eq type 'integer)
      (vector entry-name 
	      (proof-defintset-fn pasym)
	      t))
     ((eq type 'string)
      (vector entry-name 
	      (proof-defstringset-fn pasym)
	      t)))))

(defun proof-defpacustom-fn (name val args)
  "As for macro `defpacustom' but evaluation arguments."
  (let (newargs setting)
    (while args
      (cond 
       ((eq (car args) :setting)
	(setq setting (cadr args))
	(setq args (cdr args)))
       ((eq (car args) :type)
	(setq type (cadr args))
	(setq newargs (cons (car args) newargs)))
       (t
	(setq newargs (cons (car args) newargs))))
      (setq args (cdr args)))
    (setq newargs (reverse newargs))
    (unless setting
      (error "defpacustom: missing :setting keyword"))
    (unless (and type
		  (or (eq (eval type) 'boolean) 
		      (eq (eval type) 'integer) 
		      (eq (eval type) 'string)))
      (error "defpacustom: missing :type keyword or wrong :type value"))
    (if (assoc name proof-assistant-settings)
	(error "defpacustom: Proof assistanting setting %s already defined!"
	       name))
    ;; Could consider moving the bulk of the remainder of this
    ;; function to a function proof-assistant-setup-settings which
    ;; defines the custom vals *and* menu entries.   This would
    ;; allow proof assistant customization to manipulate
    ;; proof-assistant-settings directly rather than forcing
    ;; use of defpacustom.  (Probably stay as we are: more abstract)
    (eval
     `(defpgcustom ,name ,val
	,@newargs
	:set 'proof-set-value
	:group 'proof-assistant-setting))
    (eval
     `(defpgfun ,name ()
	(proof-assistant-invisible-command-ifposs
	 (proof-assistant-settings-cmd (quote ,name)))))
    (setq proof-assistant-settings
	  (cons (list name setting (eval type)) proof-assistant-settings))))

;;;###autoload
(defmacro defpacustom (name val &rest args)
  "Define a setting NAME for the current proof assitant, default VAL.
NAME should correspond to some internal setting, flag, etc, for the
proof assistant.  
The :type of NAME should be one of 'integer, 'boolean, 'string.
The customization variable is automatically in group `proof-assistant-setting.
The function `proof-assistant-format' is used to format VAL."
  `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args)))

(defun proof-assistant-invisible-command-ifposs (cmd)
  "Send CMD as an \"invisible command\" if the proof process is available."
  ;; FIXME: better would be to queue the command, or even interrupt a
  ;; queue in progress.  Also must send current settings at start of
  ;; session somehow.  (This might happen automatically if a queue of
  ;; deffered commands is set, since defcustom calls proof-set-value
  ;; even to set the default/initial value?)
  (if (proof-shell-available-p)
      (progn
	(proof-shell-invisible-command cmd t)
	;; refresh display, 
	;; FIXME: should only do if goals display is active,
	;; messy otherwise. 
	;; (we need a new flag for "active goals display").  
	(proof-prf) 
	;;  Could also repeat last command if non-state destroying.
	)))


(defun proof-assistant-settings-cmd (&optional setting)
  "Return string for making setting vals kept in Proof General customizations.
If SETTING is non-nil, return a string for just that setting. 
Otherwise return a string for configuring all settings."
  (let
      ((evalifneeded (lambda (expr)
			(if (or (not setting) 
				(eq setting (car expr)))
			    (proof-assistant-format 
			     (cadr expr) 
			     (eval (proof-ass-symv (car expr))))))))
    (apply 'concat (mapcar evalifneeded 
			   proof-assistant-settings))))

(defun proof-assistant-format (string curvalue)
  "Replace a format characters %b %i %s in STRING by formatted CURVALUE.
Formatting suitable for current proof assistant, controlled by
`proof-assistant-format-table' which see.
Finally, apply `proof-assistant-setting-format' if non-nil.
As a special case for boolean settings: the setting STRING 
can be a cons cell of two strings, the first one for true (non-nil
value) and the second for false."
  (if (consp string)
      (if curvalue (car string) (cdr string))
    ;; Otherwise must use % format characters
    (let ((setting (proof-format proof-assistant-format-table string)))
      (if proof-assistant-setting-format
	  (funcall proof-assistant-setting-format setting)
	setting))))

(defvar proof-assistant-format-table 
  (list
   (cons "%b" '(proof-assistant-format-bool curvalue))
   (cons "%i" '(proof-assistant-format-int curvalue))
   (cons "%s" '(proof-assistant-format-string curvalue)))
  "Table to use with `proof-format' for formatting CURVALUE for assistant.
NB: variable curvalue is dynamically scoped (used in proof-assistant-format).")

(defun proof-assistant-format-bool (value)
  (if value proof-assistant-true-value proof-assistant-false-value))

(defun proof-assistant-format-int (value)
  (funcall proof-assistant-format-int-fn value))

(defun proof-assistant-format-string (value)
  (funcall proof-assistant-format-string-fn value))

   


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