Re: [isabelle] Autocompletion in 2013-1

On Thu, 24 Oct 2013, Joachim Breitner wrote:

I have upgraded to 2013-1, and found that autocompletion did not work as
     * Previously, I could type "bul<TAB>" to get ∙, now I have to
       write "\bul<TAB>" or "\<bul<TAB>".
     * There were very useful shortcuts like "=_<TAB>" for \<^bsub>,
       these seem to be missing right now.

Is that just a stetting somewhere whose default has changed or is there
a deeper reason and a new way to enter such things efficiently?

The completion mechanism is all new and it is worth experimenting a bit with its options, to see what is most productive for your mode of working.

In Isabelle2013-1-RC4 the "jedit" manual in the Documentation panel provides some more explanations, although many fine points of the new mechanism are probably not immediately clear.

Extra backslashes for symbols clearly indicate the intention to prefer a replacement. The "immediate" mode of completion (disabled by default) replaces \bu on the spot, but not any prefixes of plain keywords words without special characters.


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