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

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.


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