diff options
| author | Cyril Anaclet | 2020-05-18 13:33:57 +0200 |
|---|---|---|
| committer | Anaclet | 2020-05-29 11:05:58 +0200 |
| commit | 04aff704f3d13452bc5c52ff860c5ab564539632 (patch) | |
| tree | b20a0c1ddd1b1ade477dab74a22491f1c313e8a8 | |
| parent | aba3f2bfe2bffde6d2df21b098740100459a84be (diff) | |
WIP for #487
| -rw-r--r-- | coq/coq-syntax.el | 3 | ||||
| -rw-r--r-- | generic/proof-shell.el | 7 |
2 files changed, 5 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index a27274c5..3ae7fbca 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1305,8 +1305,7 @@ It is used: (defconst coq-show-proof-diffs-regexp - ;; FIXME/TODO: enhance this regexp - "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)") + "^[ ]*Show Proof\\( Diffs\\| Diffs removed\\)?\\.$") (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b6bf9225..8f23608a 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1193,7 +1193,8 @@ contains only invisible elements for Prooftree synchronization." (or (null proof-action-list) (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list))))))) + proof-action-list) + (string= (car (nth 1 item)) "Show."))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1715,7 +1716,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output both)) + (pg-goals-display proof-shell-last-goals-output t)) ;; indicate a goals output has been given 'goals)) |