[nongnu] elpa/proof-general 57a9d9ea91 05/25: qrhl: support for several commands on the same line.

[ELPA Syncer]

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

    qrhl: support for several commands on the same line.
---
 qrhl/qrhl.el | 40 ++++++++++++++++++++++++++++++++--------
 1 file changed, 32 insertions(+), 8 deletions(-)

diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el
index 7eef34d06e..bbd93b489d 100644
--- a/qrhl/qrhl.el
+++ b/qrhl/qrhl.el
@@ -16,12 +16,36 @@
             )
        focus-cmd))
 
+(defun qrhl-forward-regex (regex)
+  "If text starting at point matches REGEX, move to end of the match and 
return t. 
+   Otherwise return nil"
+  (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).
+   Returns t if this worked."
+  (let ((pos 
+        (save-excursion 
+          (progn
+           (while (or
+                     ; skip forward over regular chars, period with non-white, 
quoted string
+                   (qrhl-forward-regex "\\([^.{(\"]+\\|\\.[^ 
\t\n]\\|\"\\([^\"]+\\)\"\\)")
+                   (and (looking-at "[{(]") (forward-list))
+                   ))
+           (and (qrhl-forward-regex "\\.") (point))
+           ))))
+    (princ pos)
+    (and pos (goto-char pos) t)))
+
+(defun qrhl-parse-focus-command ()
+  (and (looking-at qrhl-focus-cmd-regexp)
+       (goto-char (match-end 0))))
+
 (defun qrhl-proof-script-parse-function ()
-  "Finds the command starting at the point"
-  (or (and (looking-at qrhl-focus-cmd-regexp)
-          (goto-char (match-end 0))
-          'cmd)
-      (proof-script-generic-parse-cmdend)))
+  "Finds the command/comment starting at the point"
+  (or (and (qrhl-forward-regex "#[^\n]*\n") 'comment)
+      (and (qrhl-parse-focus-command) 'cmd)
+      (and (qrhl-parse-regular-command) 'cmd)))
 
 (proof-easy-config 'qrhl "qRHL"
                   proof-prog-name (concat qrhl-home "bin/qrhl")
@@ -29,11 +53,11 @@
                   ; 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-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-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