Re: [isabelle] Autocompletion in 2013-1

On Thu, 24 Oct 2013, Joachim Breitner wrote:

     * There were very useful shortcuts like "=_<TAB>" for \<^bsub>,
       these seem to be missing right now.

I don't see any change here between Isabelle2013 and Isabelle2013-1-RC4: the abbreviations are as follows:

  \<^bsub>   abbrev: =_(
  \<^esub>   abbrev: =_)
  \<^bsup>   abbrev: =^(
  \<^esup>   abbrev: =^)

It is nonetheless hard to enter both "brackets". I recommend something like the SuperAbbrevs plugin of jEdit.

The change of symbol abbreviations actually affects plain \<^sub> etc. which are much simplified. The preferred input method is via jEdit keyboard shortcuts, as explained in section 2.6 of the "jedit" manual. This only works for the main text area; completion within a text field, e.g. "Find / Seach criteria" may fall-back on plain \sub, \sup, \bold.


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