[nongnu] elpa/proof-general 3f5fe71e52 3/7: Miscelleaneous cleanup in qrhl.el (by @monnier)

[ELPA Syncer]

branch: elpa/proof-general
commit 3f5fe71e522cc61536f7256e299f21a70a54a3c3
Author: Dominique Unruh <unruh@ut.ee>
Commit: Dominique Unruh <unruh@ut.ee>

    Miscelleaneous cleanup in qrhl.el (by @monnier)
---
 qrhl/qrhl.el | 71 +++++++++++++++++++++++++++++++++---------------------------
 1 file changed, 39 insertions(+), 32 deletions(-)

diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el
index 41a9327c8f..58bc989d26 100644
--- a/qrhl/qrhl.el
+++ b/qrhl/qrhl.el
@@ -16,16 +16,19 @@
 
 (require 'proof)
 (require 'proof-easy-config)
+(require 'proof-script)                 ;For proof-generic-count-undos.
 
 (if (version< emacs-version "26")
     (require 'qrhl-input-25)
   (require 'qrhl-input))
 
 
-(defcustom qrhl-input-method "qrhl" "Input method to use when editing qRHL 
proof scripts"
+(defcustom qrhl-input-method "qrhl"
+  "Input method to use when editing qRHL proof scripts"
   :type '(string) :group 'qrhl)
 
-(defcustom qrhl-prog-name "qrhl" "Name/path of the qrhl-prover command. 
(Restart Emacs after changing this.)"
+(defcustom qrhl-prog-name "qrhl"
+  "Name/path of the qrhl-prover command. (Restart Emacs after changing this.)"
   :type '(string) :group 'qrhl)
 
 (defun qrhl-find-and-forget (span)
@@ -47,10 +50,11 @@
   (and (looking-at regex) (goto-char (match-end 0)) t))
 
 (defun qrhl-parse-regular-command ()
-  "Finds the period-terminated command starting at the point (and moves to its 
end).
+  "Find the period-terminated command starting at point.
+   Moves to its end.
    Returns t if this worked."
-  (let ((pos 
-        (save-excursion 
+  (let ((pos
+        (save-excursion
           (progn
            (while (or
                      ; skip forward over regular chars, period with non-white, 
quoted string
@@ -89,33 +93,36 @@
   "Font-lock configuration for qRHL proof scripts")
 
 (proof-easy-config 'qrhl "qRHL"
-                  proof-prog-name qrhl-prog-name
-                  ; We need to give some option here, otherwise 
proof-prog-name is interpreted
-                  ; as a shell command which leads to problems if the path 
contains spaces
-                  ; (see the documentation for proof-prog-name)
-                  qrhl-prog-args '("--emacs")
-                  ;proof-script-command-end-regexp "\\.[ \t]*$"
-                  proof-script-parse-function 'qrhl-proof-script-parse-function
-                  proof-shell-annotated-prompt-regexp 
"^\\(\\.\\.\\.\\|qrhl\\)> "
-                  ;proof-script-comment-start-regexp "#"
-                  ;proof-script-comment-end "\n"
-                  proof-shell-error-regexp "^\\(\\[ERROR\\]\\|Exception\\)"
-                  proof-undo-n-times-cmd "undo %s."
-                  proof-find-and-forget-fn 'qrhl-find-and-forget
-                  proof-shell-start-goals-regexp "^[0-9]+ 
subgoals:\\|^Goal:\\|^No current goal\\.\\|^In cheat mode\\.\\|^No focused 
goals (use "
-                  proof-shell-proof-completed-regexp "^No current goal.$"
-                  proof-shell-eager-annotation-start "\\*\\*\\* "
-                  proof-shell-eager-annotation-start-length 4
-                  proof-no-fully-processed-buffer t
-                  proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . 
"\\\""))
-                  proof-shell-cd-cmd "changeDirectory \"%s\"."
-                  proof-save-command-regexp "^adfuaisdfaoidsfasd" ; 
ProofGeneral produces warning when this is not set. But we don't want goal/save 
commands to be recognized because that makes ProofGeneral do an atomic undo.
-                  proof-tree-external-display nil
-                  proof-script-font-lock-keywords qrhl-font-lock-keywords
-                  proof-goals-font-lock-keywords qrhl-font-lock-keywords
-                  proof-response-font-lock-keywords qrhl-font-lock-keywords
-                  proof-shell-unicode t
-                  )
+  proof-prog-name qrhl-prog-name
+  ;; We need to give some option here, otherwise `proof-prog-name' is
+  ;; interpreted as a shell command which leads to problems if the file name
+  ;; contains spaces (see the documentation for `proof-prog-name').
+  qrhl-prog-args '("--emacs")
+  ;;proof-script-command-end-regexp "\\.[ \t]*$"
+  proof-script-parse-function #'qrhl-proof-script-parse-function
+  proof-shell-annotated-prompt-regexp "^\\(\\.\\.\\.\\|qrhl\\)> "
+  ;;proof-script-comment-start-regexp "#"
+  ;;proof-script-comment-end "\n"
+  proof-shell-error-regexp "^\\(\\[ERROR\\]\\|Exception\\)"
+  proof-undo-n-times-cmd "undo %s."
+  proof-find-and-forget-fn 'qrhl-find-and-forget
+  proof-shell-start-goals-regexp "^[0-9]+ subgoals:\\|^Goal:\\|^No current 
goal\\.\\|^In cheat mode\\.\\|^No focused goals (use "
+  proof-shell-proof-completed-regexp "^No current goal.$"
+  proof-shell-eager-annotation-start "\\*\\*\\* "
+  proof-shell-eager-annotation-start-length 4
+  proof-no-fully-processed-buffer t
+  proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\""))
+  proof-shell-cd-cmd "changeDirectory \"%s\"."
+  ;; ProofGeneral produces warning when this is not set.  But we don't want
+  ;; goal/save commands to be recognized because that makes ProofGeneral do an
+  ;; atomic undo.
+  proof-save-command-regexp "\\`a\\`"   ;AKA `regexp-unmatchable' in Emacs-27
+  proof-tree-external-display nil
+  proof-script-font-lock-keywords qrhl-font-lock-keywords
+  proof-goals-font-lock-keywords qrhl-font-lock-keywords
+  proof-response-font-lock-keywords qrhl-font-lock-keywords
+  proof-shell-unicode t
+  )
 
 ; buttoning functions follow https://superuser.com/a/331896/748969
 (define-button-type 'qrhl-find-file-button