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
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.
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