branch: elpa/proof-general
commit 57a9d9ea9148f058a7a84566fd1a89c225c7cea5
Author: Dominique Unruh <[email protected]>
Commit: Dominique Unruh <[email protected]>
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
