[isabelle-dev] NEWS: Dockable window "Find"

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Dockable window "Find" provides query operations for formal entities
(GUI front-end to 'find_theorems' command).


This refers to Isabelle/90edb0669845.  The main point here is the concept 
of "query operations" behind the scenes.  It allows to integrate one-shot 
print commands into the asynchronous/parallel document model. The GUI 
panel then looks mostly conventional, but with some fine points in the 
semantics: the user does not have to wait for start nor finish of the 
query.  It is all flowing in timeless/stateless space.

The panel should be basically usable, although some fine points are still 
expected to show up.  I am also curious to see what the student by Fabian 
will deliver in approx. 10 days.  We might brush up the GUI further, based 
on this project.


Anyway, what is the purpose of the find_theorems rem_dups / with_dups 
option?  I have made a tooltip that says "Allow duplicates in result 
(faster for large theories)", although I am unsure if this is correct. 
The result with duplicates is quite different, i.e. not sorted according 
to the usual heuristics.

Is this special "Duplicates" treatment still relevant?  Already for 
Isabelle2013 I've put some Par_List.map combinators in place, both for 
filter evaluation and pretty printing of the result.  Can anyone with 
access to secret benchmarks try how well this crunches on 8 or 16 cores?


 	Makarius