diff options
author | Makarius Wenzel <makarius@sketis.net> | 2007-08-15 17:26:02 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2007-08-15 17:26:02 +0000 |
commit | 3449ecf31c2cc19e3e8152183f4c0acdc6f5b532 (patch) | |
tree | 19a47a740de63453f3f7b19e661dfdce39e865ef /isar/isar.el | |
parent | fecff511bb9fd00267ad9d0d547a64e012480908 (diff) |
isar-goalhyplit-test: explicit end-marker;
Diffstat (limited to 'isar/isar.el')
-rw-r--r-- | isar/isar.el | 7 |
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)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |