diff options
| author | David Aspinall | 2001-09-24 10:23:36 +0000 |
|---|---|---|
| committer | David Aspinall | 2001-09-24 10:23:36 +0000 |
| commit | 4ff0c15856641bd69e0994319eba89be10726a2d (patch) | |
| tree | 4fb3a6d9f4f02001a0f8bd262c0e6c28fbdf2c78 | |
| parent | 49a1aaee705511633629709681b2fb1a7253eb05 (diff) | |
Implement Robert Schnecks idea to help Coq display whole of goals output.
| -rw-r--r-- | generic/proof-shell.el | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b47ed938..c9ea37f7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -955,9 +955,18 @@ which see." ;; Find the last goal string in the output (while (string-match proof-shell-start-goals-regexp string start) (setq start (match-end 0))) - ;; Convention: provers with special characters don't include - ;; the match in their goals output. Others do. - (unless proof-shell-first-special-char + ;; Convention: provers with special characters appearing in + ;; proof-start-goals-regexp don't include the match in their + ;; goals output. Others do. + ;; (Improvement to examine proof-start-goals-regexp suggested + ;; for Coq by Robert Schneck because Coq has specials but + ;; doesn't markup goals output specially). + (unless (and + proof-shell-first-special-char + (not (string-equal + proof-shell-start-goals-regexp + (proof-shell-strip-special-annotations + proof-shell-start-goals-regexp)))) (setq start (match-beginning 0))) (setq end (if proof-shell-end-goals-regexp (string-match proof-shell-end-goals-regexp string start) |