Re: [isabelle] Autocompletion in 2013-1



Hi,

Am Donnerstag, den 07.11.2013, 21:27 +0100 schrieb Makarius:
> 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.

Thanks, I’ll try that option. Together with \ it feels quite natural (if
“\” means that I want to enter a symbol, I’m fine with jEdit inserting
it as soon as it is unique). I’m not sure I like that it would also
replace (=, without a \ first.

Would it make sense to offer an option to have the immediate behavior
for symbols starting with \ only?

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

I got used to =_, but I’ll try to get used to Ctrl-E Down, so thanks for
the information.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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