diff options
| author | David Aspinall | 2007-08-19 11:18:48 +0000 |
|---|---|---|
| committer | David Aspinall | 2007-08-19 11:18:48 +0000 |
| commit | 346b2bf9593bee26e2d3d4f2319df38a92fe9112 (patch) | |
| tree | f745c1e1bd2a6ad84971c9dbfec862a9e5457739 | |
| parent | 38439769313adf1ff40a946adeaa0ece534ddaae (diff) | |
pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing markup (special 377).
| -rw-r--r-- | isar/isar.el | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/isar/isar.el b/isar/isar.el index 9c717941..a1a73731 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -144,7 +144,7 @@ See -k option for Isabelle interface script." (defun isar-shell-mode-config-set-variables () "Configure generic proof shell mode variables for Isabelle/Isar." (setq - pg-topterm-regexp "\375\\|\^AV" + pg-topterm-regexp "\376\\|\^AW" pg-topterm-goalhyplit-fn 'isar-goalhyplit-test proof-shell-wakeup-char nil @@ -635,10 +635,13 @@ Checks the width in the `proof-goals-buffer'" (proof-goals-config-done)) (defun isar-goalhyplit-test () - "This is a value for pg-topterm-goalhyplit-fn, see proof-config.el for docs." + "Value for `pg-topterm-goalhyplit-fn' (see that variable for documentation)." (let ((start (point))) - (and (proof-re-search-forward "\375\\|\^AW" nil t) - (cons 'lit (buffer-substring start (match-beginning 0)))))) + (if (proof-re-search-forward "\377\\|\^AX" nil t) ;; end of literal command (non-standard) + (progn + (delete-region (match-beginning 0) (match-end 0)) + (cons 'lit (buffer-substring start (match-beginning 0))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |