Changes between Initial Version and Version 1 of Ticket #413


Ignore:
Timestamp:
Jul 26, 2011, 12:19:11 PM (13 years ago)
Author:
David Aspinall
Comment:

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

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #413

    • Property Status changed from new to closed
    • Property Resolution changed from to worksforme

  • Ticket #413 – Description

    initial v1  
    1 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.
     1This 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.
    22
    33I'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.