[isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)

[Makarius]

On Sun, 4 Aug 2013, Fabian Immler wrote:

> I think it is a good idea to inform everyone here that a current 
> student's project is about to provide a bit more advanced user interface 
> for the find theorems functionality. It should be finished in two weeks 
> time.

So far I only know about the existence of the project, but nothing about 
its contents.

I was about to ask about it today, since I have made some further progress 
to get the concepts behind these query operations right:

changeset:   52865:02a7e7180ee5
user:        wenzelm
date:        Mon Aug 05 17:14:02 2013 +0200
files:       src/Pure/PIDE/query_operation.ML src/Pure/ROOT 
src/Pure/ROOT.ML src/Pure/Tools/find_theorems.ML 
src/Tools/jEdit/lib/Tools/jedit src/Tools/jEdit/src/find_dockable.scala 
src/Tools/jEdit/src/query_operation.scala
description:
slightly more general support for one-shot query operations via 
asynchronous print functions and temporary document overlay;


Various fine points still need to be sorted out, both at the surface and 
the bottom of it.

I have started thinking about a few advanced GUI aspect, e.g. completion 
within the input text area, potentially also formal markup there.  As a 
general principle the GUI needs to work smoothly both for beginners and 
experts. GUIs should not be toys.


PS: Next time I pass by find_theorems.ML, all the dead code will be 
garbage collected.


 	Makarius