Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 12:05):

From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Makarius,

thanks for publishing 2013-1-RC1 – looks great!

I gave the new Find GUI a try. Nice to see that it supports the same
Unicode symbol Tab completions as the main editor window.

However it took me a while that the GUI counterpart of

find_theorems "..."

is to enter "..." (including the quotes!) into the GUI input form,
whereas I would have expected that I can simply enter ... without the
quotes.

Cheers,

Christoph

Email Gateway (Aug 19 2022 at 12:11):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Hi Christoph,

if you don't expect to enter quotes in the GUI input line, how do you delimit multiple patterns from each other?

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.

Email Gateway (Aug 19 2022 at 12:12):

From: Christoph LANGE <math.semantic.web@gmail.com>
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! Maybe that's the trap of a
GUI: that it suggests simplicity where the underlying commands actually
are not that simple.

Cheers,

Christoph

Email Gateway (Aug 19 2022 at 12:17):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 19 2022 at 12:18):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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

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.

Last updated: Apr 23 2024 at 12:29 UTC