Opened 13 years ago
Closed 13 years ago
#413 closed defect (worksforme)
Clicking on Find icon does not bring up input buffer
| 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 (last modified by )
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.
Change History (1)
comment:1 Changed 13 years ago by
| Description: | modified (diff) |
|---|---|
| Resolution: | → worksforme |
| Status: | new → closed |
Thanks for the report.
I tried the example as you explained it on the current RC of PG 4.1, but I cannot duplicate the problem: when I click on the "Find" icon the Emacs minibuffer (*bottom* line of the display) shows the text "Finding theorems containing: " and you can type something after the colon.
HOWEVER: note that the command does not work in Isabelle at "top level" which means that to get search results you should not process the last line of the theory (undo "end").