Custom Query (361 matches)

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...)

if you're undoing a command, "undo" will undo the largest container which ends with the command; this is not always correct behaviour, for example if our document ends halfway through a proof, or if we've made an edit which has reset the parsed container regions, then undo will try to undo the lemma, which is incorrect (and can cause prover state to become inconsistent).

one option is to look at the proof state and only undo the largest container which has been closed (processed to the point where it is discharged, e.g. lemma .... sorry).

alternatively when we do a parse we could record whether the container is closed. if we have to change the length of that container (e.g. because of an edit) then we reset the container to be open, and we don't undo it until a parse tells us its correct end location.

it is possible that i broke this (if this used to work, then it is very likely!), by adjusting the end location of containers when edits are done. however i think the changes i made were necessary. but i think what i did to break it was approximately correct.

(were we using empty children or whitespace to indicate that a container is parsed to closure? that would explain how i broke it. if so, i suggest we refactor to use a boolean "containerParsedToClosure" on a container to indicate that it is parsed to closure, rather than sticking empty containers or whitespace into the tree.)

Is it possible to have the centering behavior of the *goals* window be configurable? I see from ticket #111 that the behavior was changed recently to center on the bottom of the goal instead of the top of the hypotheses, but unfortunately a lot of things I prove end up with 50 line goals, so the old behavior (while sometimes not ideal) is still better for me.