Re: [isabelle] Isabelle2016-1-RC1: How to Disable completion popup for quotes?
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] Isabelle2016-1-RC1: How to Disable completion popup for quotes?
- From: Makarius <makarius at sketis.net>
- Date: Sat, 3 Dec 2016 15:09:50 +0100
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1
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
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