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
buffer.

--
  Peter

> 
>   -- Lars
> 






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