[isabelle] Fact completion



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.