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