Custom Query (361 matches)
Results (4 - 6 of 361)
| Ticket | Owner | Reporter | Resolution | Summary |
|---|---|---|---|---|
| #124 | fixed | Edited text doesn't update document model | ||
| Description |
Editing text doesn't always change the document model underlying. Then sending the next command sends the old text. |
|||
| #126 | fixed | Repair symbol handling | ||
| Description |
Symbol handling is currently broken, needs urgent repair. |
|||
| #156 | fixed | closing an active editor doesn't work (buggy or confusing PGRetargetableAction.setBusy()) | ||
| Description |
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...) |
|||
