[isabelle] Fact completion
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and