aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar.el
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2007-08-15 17:26:02 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2007-08-15 17:26:02 +0000
commit3449ecf31c2cc19e3e8152183f4c0acdc6f5b532 (patch)
tree19a47a740de63453f3f7b19e661dfdce39e865ef /isar/isar.el
parentfecff511bb9fd00267ad9d0d547a64e012480908 (diff)
isar-goalhyplit-test: explicit end-marker;
Diffstat (limited to 'isar/isar.el')
-rw-r--r--isar/isar.el7
1 files changed, 3 insertions, 4 deletions
diff --git a/isar/isar.el b/isar/isar.el
index 2b9ee8d0..7a1b9a4b 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -637,10 +637,9 @@ Checks the width in the `proof-goals-buffer'"
(defun isar-goalhyplit-test ()
"This is a value for pg-topterm-goalhyplit-fn, see proof-config.el for docs."
;; We need to find the end of the proof command on the current line.
- (let ((bol (point)))
- (end-of-line) ;; could search backwards for regexps here, return nil to fail
- ;; Indicate that this is a literal command to send back
- (cons 'lit (buffer-substring bol (point)))))
+ (let ((start (point)))
+ (and (proof-re-search-forward "\375\\|\^AW" nil t)
+ (cons 'lit (buffer-substring start (match-beginning 0))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;