Re: [isabelle] 2013-1-RC1 'Find' GUI should wrap query string into "..."



Would it be possible to show an example input when there is no find theorems output?

Something that shows a few of the possible combinations, e.g.

"_ = _" "op +" name: Group -name: monoid

Cheers,
Gerwin


On 04.10.2013, at 8:12 PM, Makarius <makarius at sketis.net> wrote:

> On Fri, 4 Oct 2013, Christoph LANGE wrote:
>
>> 2013-10-04 01:38 Gerwin Klein:
>>> if you don't expect to enter quotes in the GUI input line, how do you delimit multiple patterns from each other?
>>
>> Oh, I didn't even know that you could pass multiple patterns to find_theorems – thanks for pointing out!
>
> What is missing here is a slightly more explicit explanation what find dialog expects as input.
>
> The NEWS file says "GUI front-end to 'find_theorems' command", and every Isabelle expert knows immediately that the syntax of that is documented in the isar-ref manual (although the GUI wrapper only uses the "thmcriterium" for the text field, while the other options are buttons).
>
> I still have some free space to fill in the new "jedit" manual.  The release candidates essentially freeze the whole code base, but additions to the documentation are still possible.
>
>
>> Maybe that's the trap of a GUI: that it suggests simplicity where the underlying commands actually are not that simple.
>
> That is an important observation in general.  The first encounter to the system is getting more and more easy, but working with it still requires acquaintance with many details.
>
> The general approach of Isabelle/jEdit is to deliver a system for experts, while it is made reasonably easy for beginners to become experts as well.
>
>
>       Makarius


________________________________

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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.