On 09/08/2013, at 9:17 PM, Makarius <[email protected]> wrote: > On Fri, 9 Aug 2013, Gerwin Klein wrote: > >>> Is this special "Duplicates" treatment still relevant? >> >> Yes, it's still relevant. One of the uses of the command where duplicates >> are reported is to see how often the same theorem is proved under different >> names, which these are, and how to best consolidate them. It's usually used >> with narrow search parameters, so that the result lists tend to be small. >> It's less about the speed of the output (that may have been a consideration >> very early on, but not in the last years). > > OK, can you rephrase this as a tooltip text? (Following the style of the > other tooltips.)
Done, see de4bccddcdbd 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? 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
