Common toggles

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

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

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

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,

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"))))
-
 
 
 

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.

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" "\

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

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)