path: root/generic/proof-menu.el

;; proof-menu.el  Menus, keymaps, and misc commands for Proof General
;;
;; Copyright (C) 2000,2001 LFCS Edinburgh. 
;; Authors:   David Aspinall
;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $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.
Also move point to the end of the response buffer.
If in three window or multiple frame mode, display both buffers."
;; NB: with tracing buffer, might be handy to show that.
  (interactive)
  (cond
   ((or proof-dont-switch-windows proof-multiple-frames-enable)
    ;; Display both
    (proof-switch-to-buffer proof-response-buffer 'noselect)
    (set-window-point (get-buffer-window proof-response-buffer)
		      (point-max))
    (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))
   ((buffer-live-p proof-response-buffer)
    ;; Response buffer invisible, let's display it
    (proof-switch-to-buffer proof-response-buffer 'noselect)
    (set-window-point (get-buffer-window proof-response-buffer)
		      (point-max)))
   (t
    ;; No buffers existing, do nothing (might crank up process)
    nil)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; 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-backward-command)
(define-key map [(meta e)] 'proof-forward-command)
(define-key map [(meta up)] 'proof-backward-command)
(define-key map [(meta down)] 'proof-forward-command)
(define-key map [(control meta a)] 'proof-goto-command-start)
(define-key map [(control meta e)] 'proof-goto-command-end)
(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)
(define-key map [(control c) v] 'pg-toggle-visibility);; FIXME: FSF??
(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 [(control 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)
(define-key map [(control c) (control ?\;)] 'pg-insert-last-output-as-comment)
;;
;; Experimental: span moving functions
(if proof-experimental-features (progn
      (define-key map [(control meta up)] 'pg-move-region-up)
      (define-key map [(control meta down)] 'pg-move-region-down)))
;; 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"
   proof-main-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 menus
;;;

(defvar proof-help-menu
  '("Help"
    ["PG Info"      	(info "ProofGeneral") t]
    ["PG Homepage"  	(browse-url proof-general-home-page) t]
    ["About PG"        proof-splash-display-screen t]
    ["Send Bug Report" proof-submit-bug-report t])
  "Proof General help menu.")

(defvar proof-buffer-menu
  (cons "Buffers"
	(append
	 '(["Goal or Response"
	    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)])
	 ;; FIXME: this next test doesn't work since menus
	 ;; loaded before proof-shell-trace-output-regexp is
	 ;; set (in proof-shell hook).  Should be better with
	 ;; simplified customization mechanism.
	 ;; ( if proof-shell-trace-output-regexp ... )
	   '(["Trace"
	      (proof-switch-to-buffer proof-trace-buffer)
	      :active (buffer-live-p proof-trace-buffer)])))
  "Proof General buffer menu.")

;; Make the togglers used in options menu below

(proof-deftoggle proof-dont-switch-windows)
(proof-deftoggle proof-script-fly-past-comments)
(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-disappearing-proofs)
(proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)

(defvar proof-quick-opts-menu
  (cons 
   "Options"
   '(["Disppearing Proofs" proof-disappearing-proofs-toggle 
      :style toggle
      :selected proof-disappearing-proofs]
     ["Three Window Mode" proof-dont-switch-windows-toggle
      :active (not proof-multiple-frames-enable)
      :style toggle
      :selected proof-dont-switch-windows]
     ["Delete Empty Windows" proof-delete-empty-windows-toggle
      :active (not proof-multiple-frames-enable)
      :style toggle
      :selected proof-delete-empty-windows]
     ["Multiple Frames" proof-multiple-frames-toggle
      :active (display-graphic-p)
      :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 (or (featurep 'toolbar) (featurep 'tool-bar))
		   (boundp 'proof-buffer-type)
		   ;; only allow toggling of toolbar enable in one
		   ;; buffer to avoid strange effects because we
		   ;; only keep one flag.  (Strange effects because 
		   ;; we only turn it off in one buffer at a time)
		   (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)]
     ["Fly Past Comments" proof-script-fly-past-comments-toggle
      :active (not proof-script-use-old-parser)
      :style toggle
      :selected proof-script-fly-past-comments]
     ("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)])
     ["Save Options" 
      custom-save-all ; proof-quick-opts-save  [ see comments therein ]
      t]))
  "Proof General quick options.")

(defun proof-quick-opts-save ()
  "Save current values of PG Options menu items using Custom."
  ;; Adapted from menu-bar-options-save in menu-bar.el (GNU Emacs).
  ;; BUT: that turns out to be a daft function, I think.
  ;; FIXME: investigate that in latest GNU and report as a 
  ;; possible bug.
  (interactive)
  (dolist (elt (list
		'proof-disappearing-proofs 
		'proof-multiple-frames-enable
		'proof-dont-switch-windows
		'proof-delete-empty-windows
		'proof-multiple-frames-enable
		'proof-output-fontify-enable
		'proof-toolbar-enable
		'proof-script-fly-past-comments
		(proof-ass-sym x-symbol-enable)
		'proof-follow-mode))
    (if (or
	 ;; XEmacs way: see custom-save-variables in cus-edit.el
	 (let ((spec (car-safe (get elt 'theme-value))))
	   (or
	    (and spec
		 (eq (car spec) 'user)
		 (eq (second spec) 'set))
	    (and (null spec) (get elt 'saved-value))))
	 ;; Emacs way: surely fails for vals set to nil.
	 (default-value elt))
	;; Oh dear: call to save-variable results in setting with set
	;; function, then saving, writing the whole file out numerous
	;; times and anyway saves all changes!
	(customize-save-variable elt (default-value elt)))))

(defconst proof-config-menu
  (list "----"
	;; buffer menu might better belong in toolbar menu?
	proof-buffer-menu
	proof-quick-opts-menu
	;; NB: customize-menu-create was buggy in earlier 
	;; Emacs 21.X; okay since 21.1.1
	(customize-menu-create 'proof-general)
	(customize-menu-create 'proof-general-internals 
			       "Internals"))
  "Proof General configuration menu.")

(defvar proof-menu  
  '("----"
    ["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])
  "The Proof General generic menu for scripting buffers.")


(defvar proof-main-menu
  (cons proof-general-name
	(append
	 proof-toolbar-scripting-menu
	 proof-menu
	 proof-config-menu
	 (list proof-help-menu)))
  "PG main menu used in scripting buffers.")

(defvar proof-aux-menu
  (cons proof-general-name 
	(append
	 proof-toolbar-scripting-menu
	 proof-config-menu
	 (list proof-help-menu)))
  "PG auxiliary menu used in non-scripting buffers.")




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Favourites mechanism for prover-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]
			   ["Delete Favourite" 
			    (call-interactively 
			     'proof-del-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.")

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

(defun proof-del-favourite (menuname)
  "Delete \"favourite\" command recorded at MENUNAME."
  (interactive
   (list
    (completing-read "Menu item to delete: " 
		     (mapcar 'cddr (proof-ass favourites))
		     nil t)))
  (let*
      ((favs       (proof-ass favourites))
       (rmfavs	   (remove-if 
		    (lambda (f) (string-equal menuname (caddr f)))
		    favs)))
    (unless (equal favs rmfavs)
      (easy-menu-remove-item proof-assistant-menu 
			     '("Favourites") menuname)
      (customize-save-variable  (proof-ass-sym favourites) rmfavs))))
  
(defun proof-read-favourite ()
  (let* 
      ((favs   (symbol-value (proof-ass-sym favourites)))
       (guess  (buffer-substring (save-excursion
				   (beginning-of-line-text)
				   (point)) (point)))
       (cmd (read-string
	     (concat "Command to send to " proof-assistant ": ") 
	     guess
	     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
	     proof-make-favourite-menu-history))
       (key (if (y-or-n-p "Set a keybinding for this command? : ")
		;; FIXME: better validation here would be to check
		;; this is a new binding, or remove old binding below.
		(events-to-keys
		 (read-key-sequence 
		  "Type the key to use (binding will be C-c C-a <key>): " 
		  nil t)))))
    ;; result
    (list cmd ins men key)))
	  

(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 (proof-read-favourite))
  (let*
      ((menu-entry (proof-def-favourite command inscript menuname key t))
       (favs       (proof-ass favourites))
       (rmfavs	   (remove-if 
		    (lambda (f) (string-equal menuname (caddr f)))
		    favs))
       (newfavs    (append 
		    favs 
		    (list (list command inscript menuname key)))))
    ;; If def succeeds, add to customize var and save immediately.
    (customize-save-variable  (proof-ass-sym favourites) newfavs)
    (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)))))

;;; autoload for compiled version: used in macro proof-defpacustom
;;;###autoload
(defun proof-defpacustom-fn (name val args)
  "As for macro `defpacustom' but evaluation arguments."
  (let (newargs setting evalform)
    (while args
      (cond 
       ((eq (car args) :setting)
	(setq setting (cadr args))
	(setq args (cdr args)))
       ((eq (car args) :eval)
	(setq evalform (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 (or setting evalform)
      (error "defpacustom: missing :setting or :eval 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))
    (if evalform
	(eval
	 `(defpgfun ,name ()
	    ,evalform))
      (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 can correspond to some internal setting, flag, etc, for the
proof assistant, in which case a :setting and :type value should be provided.
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.
If NAME corresponds instead to a PG internal setting, then a form :eval to
evaluate can be provided instead."
  `(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").  
	(if proof-showproof-command 
	    (proof-shell-invisible-command proof-showproof-command))
	;;  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 (and (cadr expr) ;; setting has PA string?
				 (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.