Email Gateway (Aug 19 2022 at 12:12): Email Gateway (Aug 19 2022 at 12:12):From: Joachim Breitner <breitner@kit.edu>
Hi,
I have upgraded to 2013-1, and found that autocompletion did not work as
before:
* 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?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:48):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 12:48):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 12:49):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC