Email Gateway (Aug 19 2022 at 10:10): Email Gateway (Aug 19 2022 at 10:10):From: Peter Lammich <lammich@in.tum.de>
How can I configure jEdit to also propose abbreviation replacement
inside words, or at least before special characters such as ' ?
In my concrete case, I'm using greek letter type variables, but whenever
I type: "'gamma", there comes no popup proposing \<gamma>.
The only workaround I currently know is something like typing "' gamma",
and then using backspace to erase the extra space again.
Best,
Peter
Email Gateway (Aug 19 2022 at 10:10):From: Makarius <makarius@sketis.net>
You can just ignore the propsition, it should be mostly non-intrusive.
See also what Isabelle2013/NEWS has to say:
For Isabelle2013, I merely made sure that \t actually works. Everything
else is then delegated to the Sidekick/Completion plugin of jEdit. It has
many options to customize its dynamic behaviour.
Completion content is provided by Isabelle/jEdit, though. It just uses
certain global tables, without contextual information.
Makarius
Email Gateway (Aug 19 2022 at 10:10):From: Peter Lammich <lammich@in.tum.de>
On Do, 2013-02-14 at 13:01 +0100, Makarius wrote:
On Thu, 14 Feb 2013, Peter Lammich wrote:
I type: "'gamma", there comes no popup proposing \<gamma>. The only
workaround I currently know is something like typing "' gamma", and then
using backspace to erase the extra space again.You can just ignore the propsition, it should be mostly non-intrusive.
Sorry if I phrased my question not clearly enough. I want jEdit to
propose the completion γ (\<gamma>) when I type "gamma".
However, it does not do so if I type "'gamma", nor on "foo_gamma" nor
"digamma".
While it probably makes sense not to get a completion proposal for
"gamma" if you type "digamma", I definitely want to have a completion
proposal when I type "'gamma", and would like to have one for
"foo_gamma".
For Isabelle2013, I merely made sure that \t actually works. Everything
else is then delegated to the Sidekick/Completion plugin of jEdit. It has
many options to customize its dynamic behaviour.
Unfortunately, I found no option that could enable completions within
words, or change what Sidekick/Completion considers to be a word.
Completion content is provided by Isabelle/jEdit, though. It just uses
certain global tables, without contextual information.
But SideKick obviously interprets the content of these tables wrt. some
context. For example, it does not propose a completion within a word:
If you type "dd", it proposes \<ddagger>, but if you type cudd, no
popup occurs. For me, it gets a problem, as the leading tick of a type
variable also inhibits the completion popup to occur.
Peter
Email Gateway (Aug 19 2022 at 10:10):From: Makarius <makarius@sketis.net>
Now I understand what you are trying to do. Isabelle/jEdit treats "'" as
part of a "word" according to the usual syntax for identifiers.
Since the application is just for a few exceptional cases, you can try to
use the on-board Abbreviation mechanism, or any other plugin. It is a
matter to explore possibilities of what is there already.
Makarius
Email Gateway (Aug 19 2022 at 10:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Peter,
You can type \<ga and that will bring it up.
If you count the shift key to get "<", that's 5 keys pressed.
That's my basic solution for getting a right delimiter when the notation
inside the delimiters ends on a character, like
\<langle>a,b\<rangle>
The \<langle> will precede a space, so you can type "lan", but for the
right side, you get "\<rangle>a,bran"
Regards,
GB
Email Gateway (Aug 19 2022 at 10:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
It gets even better. You can type <ga and it will bring up the
completion for gamma.
It's reaching over to the "\" with the little finger, followed by having
to type "<" that takes up a lot of time. Not having to type "\" is good
and will save me substantial time over a period of about 20 years.
Regards
Email Gateway (Aug 19 2022 at 10:11):From: Peter Lammich <lammich@in.tum.de>
You can type \<ga and that will bring it up.
Thanks that works
It gets even better. You can type <ga and it will bring up the
completion for gamma.
... But this leaves the "<" in place for me, and I end up with
"'<\<gamma>" in the buffer.
I really would like some escape-character that brings up the completions
even inside words, optimally with automatic replacement as I'm used from
PG.
Peter
Email Gateway (Aug 19 2022 at 10:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I jumped to conclusions and didn't actually hit the tab key to do the
completion, so that's the way it works for me also.
The key sequence "\<" is an escape-key-sequence. The bad thing about it
is that both characters use the right hand, and one of them uses the
shift key.
If you had an escape character, you would save pressing two keys if it
didn't use the shift key, and save only pressing one key if it used the
shift key.
As far as automatic replacement, I don't know about that.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:11):From: Makarius <makarius@sketis.net>
Maybe it was not clear that this refers to the built-in mechanism that is
configure via "Global Options / Abbreviations". It also has its own rules
about "word" boundaries for completions that need to be explored. There
are separate keyboard actions to activate replacement.
Makarius
Email Gateway (Aug 19 2022 at 10:12):From: Christian Sternagel <c.sternagel@gmail.com>
For this special case, the abbreviations <. and .> are very handy. Then
you also do not need any spacing.
How did I find those? Consult the "Symbol" tab in Isabelle/jEdit. Go to
the symbol you are interested in and hover the mouse over the
corresponding button. If there is an ASCII abbreviation in place, it
will be indicated by "abbrev:", e.g., "abbrev: <." for "\<langle>".
cheers
chris
Email Gateway (Aug 19 2022 at 10:12):From: Christian Sternagel <c.sternagel@gmail.com>
What you could also do is install an abbreviation that does start with a
non word character, e.g.,
\<alpha> code: 0x0003b1 group: greek abbrev: #a
in your ~/.isabelle/Isabelle2013/etc/symbols. Of course you would have
to do that for all Greek letters.
Now you can type '#a and will still get a completion suggestion for #a.
I'm not using automatic completion myself (I prefer to explicitly accept
with \t), but it should be possible to activate that via SideKick
options (sorry, I'm currently unable to investigate that due to the
"gray rectangle bug" ;) ... but that's a completely different story that
I should not have mentioned on the user mailing list... sorry for that).
cheers
chris
Email Gateway (Aug 19 2022 at 10:12):From: Makarius <makarius@sketis.net>
This refers to
https://bitbucket.org/isabelle_project/isabelle-release/issue/6/jedit-no-input-from-keyboard
which is part of the isabelle-users public Isabelle2013 RC stage.
The tracker is still open, although it turned out to be de-facto mainly a
private scratchpad by myself and Christian Sternagel.
The problem mentioned above is both due to xmonad and Sun/Oracle. I only
gradually realize all the traps and pitfalls that "alternative" Linux
desktop environments and window managers pose to applications like
Isabelle/jEdit.
Officially, Oracle Java 7 only supports regular Ubuntu Linux -- they hope
that every other distribution will just work by accident. OpenJDK is not
much better in this respect, although there are some versions with ad-hoc
patches for some window managers.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC