Email Gateway (Aug 22 2022 at 14:32): Email Gateway (Aug 22 2022 at 14:32):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I find the completion popups for " extremely annoying in Isabelle2016-1-RC1. Especially as
these popups capture the cursor up and down keys such that I have to press ESC before I
can use them after I have typed a ". How can I disable completion for this character? (I
do like the immediate completion popups for other character sequences like ==, so I don't
want to disable completion as a whole).
Best,
Andreas
Email Gateway (Aug 22 2022 at 14:46):From: Makarius <makarius@sketis.net>
On 04/11/16 14:15, Andreas Lochbihler wrote:
I find the completion popups for " extremely annoying in
Isabelle2016-1-RC1. Especially as these popups capture the cursor up and
down keys such that I have to press ESC before I can use them after I
have typed a ".
Did you get used to this behaviour in the meantime?
How can I disable completion for this character? (I do
like the immediate completion popups for other character sequences like
==, so I don't want to disable completion as a whole).
` and " are hard-wired quite deeply. I don't see a way to change that now.
The reason why " has emerged for the Isabelle2016-1 is the new
"embedded" category of outer syntax that is already used uniformly for
all kinds of "inner syntax". It allows quotes and cartouches
interchangeably.
Embedded syntax also works for the classic inner syntax of types and
terms, although very few people use that right now (including myself).
The main obstacle is somewhat accidental: problems printing proper
cartouches in LaTeX, instead of the current emulation via downsized
angle brackets.
Makarius
Email Gateway (Aug 22 2022 at 14:46):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
On 03/12/16 15:09, Makarius wrote:
On 04/11/16 14:15, Andreas Lochbihler wrote:
I find the completion popups for " extremely annoying in
Isabelle2016-1-RC1. Especially as these popups capture the cursor up and
down keys such that I have to press ESC before I can use them after I
have typed a ".Did you get used to this behaviour in the meantime?
No. I still find it very annoying. I tried to disable the popup with an abbrev in the
theory header, but that did not work, either.
abbrevs \<open>"\<close> = ""
I am actually thinking about changing the hard-wiring for my Isabelle version when the
release is out.
I still strongly prefer " over \<open> and \<close>, because " is so much easier to type
and I create unbalanced quotes all the time and fix them. A typical case is when I have
some equality statement "lhs = long rhs" followed by an apply proof attempt. When I
realise that this is going nowhere, I often select the right hand side and the apply
script and just start typing a new term, but this of course messes up the balancing.
Similar things also happen with left hand sides, but less frequently.
I'd probably be much happier to use \<open> and \<close> if the balancing was easier to
do. Say it changes the order according to the context. If I have an unbalanced \<open>,
then \<close> could become the first choice; and if there's an unbalanced \<close> ahead,
then \<open> should be the default; and if balancing is fine, then the \<open>_\<close>
block could be the default.
Andreas
How can I disable completion for this character? (I do
like the immediate completion popups for other character sequences like
==, so I don't want to disable completion as a whole).` and " are hard-wired quite deeply. I don't see a way to change that now.
The reason why " has emerged for the Isabelle2016-1 is the new
"embedded" category of outer syntax that is already used uniformly for
all kinds of "inner syntax". It allows quotes and cartouches
interchangeably.Embedded syntax also works for the classic inner syntax of types and
terms, although very few people use that right now (including myself).
The main obstacle is somewhat accidental: problems printing proper
cartouches in LaTeX, instead of the current emulation via downsized
angle brackets.Makarius
Email Gateway (Aug 22 2022 at 14:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I still strongly prefer " over \<open> and \<close>, because " is so
much easier to type.
I prefer to input \<open> and \<close> just by the vanilla keyboard
shortcuts of a typical Linux system with German keyboard layout (*):
shift + alt gr + X and shift + alt gr + Y. I am quite comfortable with
this since I also prefer French quotes »« in written text and these are
alt gr + Y and alt gr + X. What remains confusing is that for
cartouches the logic of opening and closing is reverted wrt. the
position of Y and X on the keyboard.
Cheers,
Florian
(*) I guess for English default keyboard you have to use Z instead of Y.
signature.asc
Email Gateway (Aug 22 2022 at 14:49):From: Makarius <makarius@sketis.net>
The order is correct for a German keyboard, but wrong from the French
perspective. Isabelle uses the original French orientation, but without
extra space.
Another common confusion is to call the guillemets incorrectly
"guillemots", e.g. done in Adobe font encodings and TeX/LaTeX.
See also https://fr.wikipedia.org/wiki/Guillemet
Makarius
signature.asc
Last updated: Apr 25 2024 at 16:19 UTC