Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Optional timeout warning when waiting for the proof shell #516

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Optional timeout warning when waiting for the proof shell #516

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
1f2120a
Add proof-shell-timeout-warn variables (see #514)
andyqhan Oct 12, 2020
99cd00c
Add shell-internal variable for timer (see #514)
andyqhan Oct 12, 2020
d8d6104
Implement timeout message (see #514)
andyqhan Oct 12, 2020
ebea62f
fix parentheses
andyqhan Oct 12, 2020
3ab6159
fix empty goals bug because of previous commit
andyqhan Oct 12, 2020
9a38852
change timer config to one variable
andyqhan Oct 12, 2020
f8c0c09
Change warning text to clarify C-c C-c vs C-c C-x
andyqhan Oct 13, 2020
11d8c59
cancel timer in the case of error or interrupt
andyqhan Oct 14, 2020
ae1b766
implement matafou's suggestions
Mar 21, 2021
989ef2e
Merge branch 'master' of https://github.com/ProofGeneral/PG
Mar 21, 2021
debe754
more fixes… seems to work lol
Mar 28, 2021
1cc7e70
arm timer every command, not every region
Apr 3, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Implement timeout message (see #514)
  • Loading branch information
@andyqhan
andyqhan committed Oct 12, 2020
commit d8d61044fb2329dd5f812e633170d6c52a6e6519
10 changes: 9 additions & 1 deletion generic/proof-script.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2025,7 +2025,15 @@ This function expects the buffer to be activated for advancing."
(lastpos (nth 2 (car semis)))
(vanillas (proof-semis-to-vanillas semis displayflags)))
(proof-script-delete-secondary-spans startpos lastpos)
(proof-extend-queue lastpos vanillas)))
(proof-extend-queue lastpos vanillas))

;; arm the timeout timer
;; cancelled in proof-shell-exec-loop unless proof-shell-busy
(if proof-shell-timeout-warn-p
(setq proof-shell-timer
(run-with-timer proof-shell-timeout-warn-length nil
'message "This command is taking a while. \
Is it malformed? Do C-c C-c or C-c C-x to abort."))))

(defun proof-retract-before-change (beg end)
"For `before-change-functions'. Retract to BEG unless BEG and END in comment.
Expand Down
8 changes: 7 additions & 1 deletion generic/proof-shell.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1205,7 +1205,13 @@ contains only invisible elements for Prooftree synchronization."
;; If the last command in proof-action-list is a "Show Proof" form then return t
(when last-command
(proof-shell-string-match-safe
proof-show-proof-diffs-regexp last-command)))))))))
proof-show-proof-diffs-regexp last-command))))))))

(unless proof-shell-busy
;; if the shell isn't still busy, cancel timer
(if (and proof-shell-timer proof-shell-timeout-p)
(progn (cancel-timer proof-shell-timer)
(setq proof-shell-timer nil)))


(defun proof-shell-insert-loopback-cmd (cmd)
Expand Down