diff options
Diffstat (limited to 'generic/proof-menu.el')
| -rw-r--r-- | generic/proof-menu.el | 64 |
1 files changed, 28 insertions, 36 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index df617347..fc18d504 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -1,32 +1,31 @@ ;;; proof-menu.el --- Menus, keymaps, misc commands for Proof General -;; -;; Copyright (C) 2000,2001,2009,2010,2011 LFCS Edinburgh. -;; Authors: David Aspinall -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; -(require 'cl) ; mapcan +;; This file is part of Proof General. -;;; Code: -(eval-when (compile) - (defvar proof-assistant-menu nil) ; defined by macro in proof-menu-define-specific - (defvar proof-mode-map nil)) +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel -(require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant -(require 'proof-useropts) -(require 'proof-config) +;; Authors: David Aspinall +;; License: GPL (GNU GENERAL PUBLIC LICENSE) - +;;; Commentary: +;; +;;; Code: +(require 'cl) ; mapcan (eval-when-compile (defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific (defvar proof-mode-map)) - +(require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant +(require 'proof-useropts) +(require 'proof-config) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; @@ -123,6 +122,7 @@ without adjusting window layout." ;; C-c C-v is proof-minibuffer-cmd in universal-keys ;; C-c C-. is proof-goto-end-of-locked in universal-keys (define-key map [(control c) (control return)] 'proof-goto-point) + (define-key map [(control c) (control m)] 'proof-goto-point) ; fallback for tty (define-key map [(control c) ?v] 'pg-toggle-visibility) (define-key map [(control meta mouse-3)] 'proof-mouse-goto-point) ;; NB: next binding overwrites comint-find-source-code. @@ -318,7 +318,7 @@ without adjusting window layout." (proof-deftoggle proof-delete-empty-windows) (proof-deftoggle proof-shrink-windows-tofit) (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle) -(proof-deftoggle proof-layout-windows-on-visit-file +(proof-deftoggle proof-layout-windows-on-visit-file proof-layout-windows-eagerly-toggle) (proof-deftoggle proof-three-window-enable proof-three-window-toggle) (proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle) @@ -339,11 +339,10 @@ without adjusting window layout." (proof-deftoggle-fn (proof-ass-sym unicode-tokens-enable) 'proof-unicode-tokens-toggle) (proof-deftoggle-fn - (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle) - (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle)) + (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)) (defun proof-keep-response-history () - "Enable associated buffer histories following `proof-keep-response-history'." + "Enable associated buffer histories following option `proof-keep-response-history'." (if proof-keep-response-history (proof-map-buffers (proof-associated-buffers) (bufhist-init)) (proof-map-buffers (proof-associated-buffers) (bufhist-exit)))) @@ -372,7 +371,7 @@ without adjusting window layout." ["Beep on Errors" proof-shell-quiet-errors-toggle :style toggle :selected (not proof-shell-quiet-errors) - :help "Beep on errors or interrupts"] + :help "Beep on errors or interrupts"] ["Fly Past Comments" proof-script-fly-past-comments-toggle :style toggle :selected proof-script-fly-past-comments @@ -391,7 +390,7 @@ without adjusting window layout." :style radio :selected (eq proof-autosend-all nil) :active proof-autosend-enable - :help "Automatically try out the next commmand"] + :help "Automatically try out the next command"] ["Send Whole Buffer" (customize-set-variable 'proof-autosend-all t) :style radio @@ -535,12 +534,6 @@ without adjusting window layout." :selected (and (boundp 'maths-menu-mode) maths-menu-mode) :help "Maths menu for inserting Unicode characters"] - ["Multiple Modes" (proof-mmm-toggle (if mmm-mode 0 1)) - :active (proof-mmm-support-available) - :style toggle - :selected (and (boundp 'mmm-mode) mmm-mode) - :help "Allow multiple major modes"] - ["Index Menu" proof-imenu-toggle :active (stringp (locate-library "imenu")) :style toggle @@ -588,7 +581,6 @@ without adjusting window layout." 'proof-strict-read-only (proof-ass-sym unicode-tokens-enable) (proof-ass-sym maths-menu-enable) - (proof-ass-sym mmm-enable) 'proof-toolbar-enable 'proof-keep-response-history 'proof-imenu-enable @@ -621,7 +613,7 @@ without adjusting window layout." ;; (defun proof-set-document-centred () - "Select options for document-centred working" + "Select options for document-centred working." (interactive) (proof-full-annotation-toggle 1) (proof-auto-raise-toggle 0) @@ -634,9 +626,9 @@ without adjusting window layout." (defun proof-set-non-document-centred () - "Set options for classic Proof General interaction" + "Set options for classic Proof General interaction." (interactive) - ;; default: (proof-full-annotation-toggle 1) + ;; default: (proof-full-annotation-toggle 1) (proof-auto-raise-toggle 1) (proof-colour-locked-toggle 1) (proof-sticky-errors-toggle 0) @@ -752,7 +744,7 @@ without adjusting window layout." ;;; Define stuff from favourites (defun proof-def-favourite (command inscript menuname &optional key new) - "Define and a \"favourite\" proof assisant function. + "Define and a \"favourite\" proof assistant 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. @@ -995,7 +987,7 @@ We first clear the dynamic settings from `proof-assistant-settings'." (let (cmds) (dolist (setting proof-assistant-settings) (let ((sym (car setting)) - (pacmd (cadr setting))) + (pacmd (cadr setting))) (if (and pacmd (or (not (get sym 'pgdynamic)) (proof-ass-differs-from-default sym))) @@ -1046,7 +1038,7 @@ value) and the second for false." ((consp string) ;; true/false options (if curvalue (car string) (cdr string))) (t ;; no idea what to do - (error "proof-assistant-format: called with invalid string arg %s" string))))) + (error "Function proof-assistant-format: called with invalid string arg %s" string))))) (if proof-assistant-setting-format (funcall proof-assistant-setting-format setting) setting))) |