On Mon, 2 Mar 2015, Manuel Eberl wrote:


There is also ALL and EX as already existing replacement ASCII syntax for ! and ?. I usually type ALL when I want to enter â anyway; it doesn't seem to work with EX though.


The Isabelle/jEdit manual has a long explanation on completion. The above case falls under "Input events" for "syntax keywords" (because some alphabetic text is to be replaced). It says:

\item Completion of syntax keywords requires at least 3 relevant
characters in the text.

Explicit completion always works, regardless of the input length.

Anyway, I consider the replacements of ALL, EX etc. as *very* nostalgic.

Makarius

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