diff options
| author | Pierre Courtieu | 2017-02-27 11:21:08 +0100 |
|---|---|---|
| committer | GitHub | 2017-02-27 11:21:08 +0100 |
| commit | bbc55fe1a69c9e44d2df86b447603e7972c6d238 (patch) | |
| tree | 044cc3e7f0b09e1777c808e345ff8f915a5cda95 /generic/proof-shell.el | |
| parent | bef28eaad907cb2bc4cd54fb3674a6edbe19320e (diff) | |
| parent | 0252db29c55e72bdc2c60370c29705cddced152c (diff) | |
Merge pull request #156 from Matafou/fix-154
Fixing #154.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 13da8d98..51305eef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1110,6 +1110,22 @@ contains only invisible elements for Prooftree synchronization." (setq cbitems (cons item (proof-shell-slurp-comments))) + ;; If proof-action-list is empty after removing the already + ;; processed actions and the last action was not already + ;; added by proof-shell-empty-action-list-command (prover + ;; specific), call it. + (when (and (null proof-action-list) + (not (memq 'empty-action-list flags))) + (let* ((cmd (mapconcat 'identity (nth 1 item) " ")) + (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) + ;; tag all new items with 'empty-action-list + (extra-items (mapcar (lambda (s) (proof-shell-action-list-item + s 'proof-done-invisible + (list 'invisible 'empty-action-list))) + extra-cmds))) + ;; action-list should be empty at this point + (setq proof-action-list (append extra-items proof-action-list)))) + ;; This is the point where old items have been removed from ;; proof-action-list and where the next item has not yet been ;; sent to the proof assistant. This is therefore one of the |