Email Gateway (Aug 19 2022 at 16:32): 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
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 LinkedHashSetMaybe 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: Nov 21 2024 at 12:39 UTC