Re: [isabelle] Isabelle2016-1-RC1: How to Disable completion popup for quotes?
On 03/12/16 15:09, Makarius wrote:
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.
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?
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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and