Opened 13 years ago
Last modified 13 years ago
#413 closed defect
Clicking on Find icon does not bring up input buffer — at Initial Version
| Reported by: | Generic Isabelle user | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.1 |
| Component: | 2:pg-emacs | Keywords: | Find Search |
| Cc: |
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.
