Custom Query (361 matches)
Results (43 - 45 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #8 | fixed | Cleanup active script handling in actions | ||
| Description |
Active script switching needs overhaul. Switching should be managed in UI actions and treated as part of protocol for correct use of SessionManager. SessionManager may throw exceptions if actions are tried on inactive scripts. Activity switching is carefully controlled. |
|||
| #248 | fixed | Clear error markers at correct points (e.g., when processing text successfully) | ||
| Description |
At the moment error markers are only removed when text is edited or reparsed. But it is possible to repair an error without changing the text locally: for example, theory ErrorMarkerCleaning imports Main NewTheory begin end Process this without then with NewTheory?.thy being present in the directory (see test case in ed.inf.proofgeneral.tests project). |
|||
| #413 | worksforme | Clicking on Find icon does not bring up input buffer | ||
| Description |
This problem may be due to my inexperience with emacs and/or proof general and/or isabelle, but I think at the very least it's a user-friendliness issue. I'm trying to follow the directions in the Isabelle tutorial at http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/tutorial.pdf in section 3.1.11--Finding Theorems. I load the ToyList.thy that I copied from Figure 2.1, and I process all of the proof commands in that theory. Then I press the "Find" icon. The toolbar changes and the ToyList.thy buffer seems to lose focus, but when I type, no text appears, and I cannot find a buffer that will let me enter my search text. I'm running proof general Version 4.1pre101216 on GNU Emacs 23.2.1 (i686-pc-linux-gnu, GTK+ Version 2.24.4), running on Ubuntu 11.04. |
|||
