Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Fact completion


view this post on Zulip Email Gateway (Aug 19 2022 at 16:32):

From: Lars Noschinski <noschinl@in.tum.de>
Hi,

currently I'm working on a theory where theorems often have long names,
so I have started using the fact completion mechanism of Isabelle/jEdit.
This is already a great help. However, often my lemma names have a large
common prefix, so I either have to type this one or scroll through a
large selection of lemmas.

Eclipse has a nice mechanism for such names: Names and typed text are
split in words (as Camelcase is usual in the Java world, upper-case
letters signify the beginning of a new word) and the completion suggest
all those names, for which the typed words are prefixes of the names'
words. A few examples:

* L, LH, LHS, LiHaSet would all include LinkedHashSet
* HS would include HashSet, but not LinkedHashSet

Maybe a similar mechanism (e.g., with underscore taking the role of
upper-case letters) would be a nice addition for Isabelle's IDEs?

-- Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 16:32):

From: Peter Lammich <lammich@in.tum.de>
On Do, 2014-11-27 at 17:39 +0100, Lars Noschinski wrote:

* L, LH, LHS, LiHaSet would all include LinkedHashSet
* HS would include HashSet, but not LinkedHashSet

Maybe a similar mechanism (e.g., with underscore taking the role of
upper-case letters) would be a nice addition for Isabelle's IDEs?

As would be the feature that you can continue typing while the
completion dialog is open, thus narrowing the offered choices.

In my everyday work, I use a combination of both, the Isabelle
completion, which only works in well-defined contexts that (already)
parse and in particular NOT in inner syntax, but only offers completions
that make sense, and the jedit built-in completion, which always works,
but bases its completion offers just on the words occuring in the same
buffer.


Last updated: Mar 28 2024 at 20:16 UTC