On 10/08/2013, at 9:09 AM, Gerwin Klein <[email protected]> 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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
