Re: [isabelle] Isabelle2016-1-RC1: How to Disable completion popup for quotes?

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.


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


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