Custom Query (361 matches)

if i parse a theory passed the "end" point, "undo" no longer works; ("undo all" sometimes does, but "undo" should give an error at least)

i'm also not sure it correctly registers that the theory is closed, when i switch to another theory it wouldn't let me activate it (but that could be do to a failed retract...)

if i close an active editor, the GotoAction? throws an NPE when trying to undo-all the proof script. thereafter the user cannot activate any script (even re-opening the same file) until the prover is restarted.

see comments in PGRetargetableAction.setBusy(): it looks like this call does not do what it is supposed to if the document is set manually (as it is from ActivateAction?.closeDownScript).

as a larger issue, we need to consider the different cases of closing (and re-opening) a script:

(a) if the script is fully processed, the user probably wants to keep it in the prover's memory (i.e. don't retract); however they do need a way to retract it later, probably re-opening the script should "remember" it is fully processed. (not sure what we do currently)

(b) if the script is partially processed, it is probably okay to undo all (which we currently do, modulo fixing the above bug). however it would be nicer, i think, to give the user the option to (a) discard (undo all); (b) finish processing; (c) cancel. (and maybe option to "do nothing", leave partially processed, and restoring it if they open the file later.) we used to do this, but it is commented out (in ActivateAction?). possibly because we were not getting reliably informed about shutdown events and so were pointlessly prompting the user on shutdown...)

Indentation is not closed properly after an "Abort." statement, following "Theorem".

Simple fix: In coq/coq-syntax.el: Add "Abort" to the list of keywords defined in coq-keywords-save-strict (line 618 in ProofGeneral-3.7pre071025).