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

[Gerwin Klein]

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.