diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-01-09 17:21:44 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-01-09 17:21:44 +0000 |
| commit | fbcd39419bb84b3c61fb59298f73ce4b485d5454 (patch) | |
| tree | 498f2fa90e12c2335b86d11c0af5806a33beb3f3 /generic/proof-shell.el | |
| parent | 527463db94b95e136637709561e07e59f06298c6 (diff) | |
Improve configuration for HOL Light. Allow goals display to be prefixed by ignored junk (val it : goalstack =).
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index ab0d2d05..9cdce998 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1518,11 +1518,16 @@ i.e., 'goals or 'response." (cond ((and proof-shell-start-goals-regexp (proof-re-search-forward proof-shell-start-goals-regexp end t)) - (let* ((gstart (match-beginning 0)) (rstart start) gend) + (let* ((gmark (match-beginning 0)) ; start of goals message + (gstart (or (match-end 1) ; start of actual display + gmark)) + (rstart start) ; possible response before goals + (gend end)) ;; Find the last goal string in the output (goto-char gstart) (while (re-search-forward proof-shell-start-goals-regexp end t) - (setq gstart (match-beginning 0)) + (setq gmark (match-beginning 0)) + (setq gstart (or (match-end 1) gmark)) (setq gend (if (and proof-shell-end-goals-regexp (re-search-forward proof-shell-end-goals-regexp end t)) @@ -1536,10 +1541,10 @@ i.e., 'goals or 'response." (pg-goals-display proof-shell-last-goals-output)) ;; also allow (for Coq) any preceding output as a response ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp - (when (> (- gstart rstart) 4) + (when (> (- gmark rstart) 4) (proof-shell-display-output-as-response flags - (buffer-substring-no-properties rstart gstart))) + (buffer-substring-no-properties rstart gmark))) ;; primary output kind is goals 'goals)) |