diff --git a/CHANGES b/CHANGES index dae1d8fa2..e542486f8 100644 --- a/CHANGES +++ b/CHANGES @@ -30,6 +30,11 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG `proof-goals-scroll-margin'. ** Coq changes +*** The toggle commands of the user options of Proof General + (`proof-three-window-toggle', `proof-electric-terminator-toggle'…), + of `coq-show-proof-stepwise' and of `coq-auto-adapt-printing-width' + (new `coq-auto-adapt-printing-width-toggle'), and `coq-Compile', are + defined without the proof shell, for all Coq backends. *** The compilation of the Requires before they are processed (see `coq-compile-before-require') does not depend on the proof shell any more: other Coq backends can use it, with its options and its diff --git a/ci/simple-tests/coq-test-without-pg.el b/ci/simple-tests/coq-test-without-pg.el index 51196cf50..76b129858 100644 --- a/ci/simple-tests/coq-test-without-pg.el +++ b/ci/simple-tests/coq-test-without-pg.el @@ -38,8 +38,14 @@ (defvar coq-set-search-blacklist-function) (defvar coq-search-blacklist-current-string) (defvar coq-insert-menu) +(defvar proof-output-tooltips) +(defvar proof-electric-terminator-enable) +(defvar coq-show-proof-stepwise) (declare-function coq-run-query "coq-queries") +(declare-function proof-output-tooltips-toggle "proof-useropts") +(declare-function proof-electric-terminator-toggle "proof-useropts") +(declare-function coq-show-proof-stepwise-toggle "coq-goals") (declare-function coq-templates-setup "coq-templates") (declare-function coq-terminator-insert "coq-mode") (declare-function coq-About "coq-queries") @@ -269,6 +275,39 @@ interface functions. Return released or failed." (should (equal args '("\"Private_\"" "\"foo_\""))) (should (equal coq-search-blacklist-current-string "\"foo_\""))))) +;; toggles + +(ert-deftest coq-test-without-pg-toggles () + "The toggle commands of the options are defined without PG." + (coq-test-without-pg-with-file + (require 'proof-useropts) + (require 'coq-goals) + (require 'coq-compile-common) + (dolist (command '(proof-three-window-toggle proof-output-tooltips-toggle + proof-autosend-toggle proof-electric-terminator-toggle + proof-disappearing-proofs-toggle + proof-sticky-errors-toggle + proof-omit-proofs-option-toggle + coq-show-proof-stepwise-toggle + coq-auto-adapt-printing-width-toggle + coq-Compile)) + (should (commandp command))) + (let ((proof-output-tooltips nil) + (coq-show-proof-stepwise nil)) + (proof-output-tooltips-toggle) + (should proof-output-tooltips) + (coq-show-proof-stepwise-toggle) + (should coq-show-proof-stepwise)) + ;; the electric terminator, its function and its lighter + (let ((proof-electric-terminator-enable nil)) + (proof-electric-terminator-toggle 1) + (should proof-electric-terminator-enable) + (should (stringp (format-mode-line minor-mode-alist))) + (proof-electric-terminator-toggle 0) + (should-not proof-electric-terminator-enable)) + (should-not (featurep 'proof-shell)) + (should-not (featurep 'proof-script)))) + (provide 'coq-test-without-pg) ;;; coq-test-without-pg.el ends here diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 8c7a534ac..c8f4214d7 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -786,6 +786,13 @@ current buffer (which contains the Require command) to +(defun coq-Compile () + "Compiles current buffer." + (interactive) + (let* ((n (buffer-name)) + (l (string-match ".v" n))) + (compile (concat "make " (substring n 0 l) ".vo")))) + ;;; menu (defconst coq-compile-menu diff --git a/coq/coq-goals.el b/coq/coq-goals.el index cb7c3f58a..8bf4acfab 100644 --- a/coq/coq-goals.el +++ b/coq/coq-goals.el @@ -23,6 +23,7 @@ (require 'subr-x) (require 'seq) +(require 'pg-pamacs) ; proof-deftoggle (defcustom coq-prefer-top-of-conclusion nil "Prefer start of the conclusion over its end when displaying large goals. @@ -54,6 +55,20 @@ at the width of the response window." :safe 'booleanp :group 'coq) +(proof-deftoggle coq-auto-adapt-printing-width) + +(defcustom coq-show-proof-stepwise nil + "Display the proof terms stepwise in the *response* buffer. +This option can be combined with option `coq-diffs'. +It is mostly useful in three window mode, see also +`proof-three-window-mode-policy' for details." + + :type 'boolean + :safe 'booleanp + :group 'coq-auto-compile) + +(proof-deftoggle coq-show-proof-stepwise) + (defcustom coq-optimise-resp-windows-enable t "If non-nil (default), resize the goals and response windows to their content. After each command, the response window gets the height of its content, diff --git a/coq/coq.el b/coq/coq.el index 2e3ad056a..cd93883bf 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -303,18 +303,6 @@ See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) -(defcustom coq-show-proof-stepwise nil - "Display the proof terms stepwise in the *response* buffer. -This option can be combined with option `coq-diffs'. -It is mostly useful in three window mode, see also -`proof-three-window-mode-policy' for details." - - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - -(proof-deftoggle coq-show-proof-stepwise) - ;; ;; prooftree customization ;; @@ -1091,13 +1079,6 @@ at `proof-assistant-settings-cmds' evaluation time.") (add-to-list 'proof-assistant-settings '(diffs--function "%l" string "Show Diffs in Coq") t) -(defun coq-Compile () - "Compiles current buffer." - (interactive) - (let* ((n (buffer-name)) - (l (string-match ".v" n))) - (compile (concat "make " (substring n 0 l) ".vo")))) - diff --git a/generic/pg-user.el b/generic/pg-user.el index 748634bc8..782197030 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -522,30 +522,7 @@ This is intended as a value for `proof-activate-scripting-hook'" ;; Electric terminator mode ;; -;; Register proof-electric-terminator as a minor mode. -(or (assq 'proof-electric-terminator-enable minor-mode-alist) - (setq minor-mode-alist - (append minor-mode-alist - (list '(proof-electric-terminator-enable - (:eval - (if (eq major-mode proof-mode-for-script) - proof-terminal-string))))))) - -;;;###autoload -(defun proof-electric-terminator-enable (&optional arg) - "Ensure modeline update to display new value for electric terminator. -This a function is called by the custom-set property \\+`proof-set-value'. -It can also be used as a minor mode function: with ARG, turn on iff ARG>0" - (unless (null arg) - (setq proof-electric-terminator-enable (> (prefix-numeric-value arg) 0))) - ;; the double hit is a replacement - (when (and proof-electric-terminator-enable proof-double-hit-enable) - (proof-double-hit-toggle 0) - (message "Hit M-1 . to enter a real \".\".")) - (force-mode-line-update)) - -(proof-deftoggle proof-electric-terminator-enable - proof-electric-terminator-toggle) +;; The minor mode, its function and its toggle are in proof-useropts.el. (defun proof-electric-terminator (&optional count) "Insert terminator char, maybe sending the command to the assistant. diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index e64c8c9e0..94f10c373 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -511,13 +511,6 @@ CMDVAR is a variable holding a function or string. Automatically has history. \(fn FN DOC CMDVAR PROMPT &rest BODY)" nil t) -(autoload 'proof-electric-terminator-enable "pg-user" "\ -Ensure modeline update to display new value for electric terminator. -This a function is called by the custom-set property 'proof-set-value. -It can also be used as a minor mode function: with ARG, turn on iff ARG>0 - -\(fn &optional ARG)" nil nil) - (autoload 'pg-slow-fontify-tracing-hint "pg-user" nil nil nil) (autoload 'pg-response-buffers-hint "pg-user" "\ diff --git a/generic/proof-menu.el b/generic/proof-menu.el index f9801bbae..5f2602804 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -327,26 +327,7 @@ without adjusting window layout." ;; First, make the togglers used in options menu below (proof-deftoggle proof-script-fly-past-comments) -(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-layout-windows-eagerly-toggle) -(proof-deftoggle proof-three-window-enable proof-three-window-toggle) -(proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle) -(proof-deftoggle proof-disappearing-proofs) -(proof-deftoggle proof-full-annotation) -(proof-deftoggle proof-colour-locked) -(proof-deftoggle proof-sticky-errors) -(proof-deftoggle proof-shell-quiet-errors) -(proof-deftoggle proof-minibuffer-messages) -(proof-deftoggle proof-output-tooltips) -(proof-deftoggle proof-autosend-enable proof-autosend-toggle) -(proof-deftoggle proof-fast-process-buffer) -(proof-deftoggle proof-imenu-enable proof-imenu-toggle) -(proof-deftoggle proof-keep-response-history) -(proof-deftoggle proof-omit-proofs-option) -(proof-deftoggle proof-splash-enable) +;; The togglers of the user options are in proof-useropts.el. (proof-eval-when-ready-for-assistant ;; togglers for settings separately configurable per-prover diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index ee72fb26c..545c76a6a 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -25,6 +25,8 @@ ;;; Code: +(require 'pg-pamacs) ; proof-deftoggle + (defgroup proof-user-options nil "User options for Proof General." :group 'proof-general @@ -525,6 +527,64 @@ screen is shown." :group 'proof-user-options) +;; +;; Toggle commands of the user options, for the menus of all backends +;; + +(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-layout-windows-eagerly-toggle) +(proof-deftoggle proof-three-window-enable proof-three-window-toggle) +(proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle) +(proof-deftoggle proof-disappearing-proofs) +(proof-deftoggle proof-full-annotation) +(proof-deftoggle proof-colour-locked) +(proof-deftoggle proof-sticky-errors) +(proof-deftoggle proof-shell-quiet-errors) +(proof-deftoggle proof-minibuffer-messages) +(proof-deftoggle proof-output-tooltips) +(proof-deftoggle proof-autosend-enable proof-autosend-toggle) +(proof-deftoggle proof-fast-process-buffer) +(proof-deftoggle proof-imenu-enable proof-imenu-toggle) +(proof-deftoggle proof-keep-response-history) +(proof-deftoggle proof-omit-proofs-option) +(proof-deftoggle proof-splash-enable) + +;; +;; Electric terminator mode +;; + +(declare-function proof-double-hit-toggle "pg-double-hit") +(defvar proof-mode-for-script) +(defvar proof-terminal-string) + +;; Register proof-electric-terminator as a minor mode. +(or (assq 'proof-electric-terminator-enable minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-electric-terminator-enable + (:eval + (if (and (boundp 'proof-mode-for-script) + (eq major-mode proof-mode-for-script)) + proof-terminal-string))))))) + +(defun proof-electric-terminator-enable (&optional arg) + "Ensure modeline update to display new value for electric terminator. +This a function is called by the custom-set property \\+`proof-set-value'. +It can also be used as a minor mode function: with ARG, turn on iff ARG>0" + (unless (null arg) + (setq proof-electric-terminator-enable (> (prefix-numeric-value arg) 0))) + ;; the double hit is a replacement + (when (and proof-electric-terminator-enable + (bound-and-true-p proof-double-hit-enable)) + (proof-double-hit-toggle 0) + (message "Hit M-1 . to enter a real \".\".")) + (force-mode-line-update)) + +(proof-deftoggle proof-electric-terminator-enable + proof-electric-terminator-toggle) (provide 'proof-useropts)