Re: [isabelle] Fact completion

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


>   -- Lars

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