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

[Gerwin Klein]

(Hopefully) concluding this discussion with myself, see 797362ce0c14. 

The output order just survives from the initial order in which facts are given to the search. Local facts are now passed in first, under the assumption that they will be more relevant to what the user wants to do. 

Cheers,
Gerwin

On 10/08/2013, at 11:19 AM, Gerwin Klein <Gerwin.Klein at nicta.com.au>
 wrote:

> 
> On 10/08/2013, at 9:09 AM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
>> I like the interface, it's very responsive. There is a remnant from PG times: the best match is currently the last entry in the list, which means in jEdit that you need to scroll to see it. Should we automatically scroll to the bottom or reverse the list?
> 
> Looking at this again, I'm not sure if what I wrote is actually true. I do seem to get the best matches at the top for most queries.
> 
> What triggered my observation above was that a local fact (in my case local.assms) got shown at the end of the list, even though it was the best match. Any idea where this could be coming from? I don't remember any special treatment of local facts compared to others, and looking (very) briefly over the code, I didn't see any.
> 
> The example I used was (on HOL/Main)
> 
> lemma x:
>  assumes "2 <= card S"
>  show P
> ..
> 
> using the find_theorems interface after the assumes with the search "_ <= card _" gives me a list of 15 matches, where the local assumption is the last, but the otherwise best (smallest) match is the first.
> 
> In any case, this doesn't seem to be a problem specific to the interface, but to the processing on the ML side.
> 
> Cheers,
> Gerwin
> 
> 
> ________________________________
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev