*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Another newbie question...case-based proofs*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 12 Mar 2019 16:46:55 +0000*In-reply-to*: <1552407330.8237.61.camel@jeltsch.info>*References*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com> <2315a38013d645bfa7ed4a7a37948817@chalmers.se> <D296D69F59ADF247B47C452A21D6ED2314142FD6@XMBX3.uibk.ac.at> <1552327215.3710.8.camel@in.tum.de> <9be127f9-1d5c-9673-3720-e82e46db1e21@gmail.com> <1552407330.8237.61.camel@jeltsch.info>

Hi > In general, I’d appreciate it a lot if the Isabelle IDE could be made > more comfortable for people who mostly use the keyboard and can get > on > speed with it. In particular, it would be great if the completion > mechanism could be improved. You can set "completion delay" to 0 in the options ... that's one of the first things I do when I set up a new Isabelle version! The upside is that hardcoded completions (eg unicode symbols) come up immediately. The downside is that dynamic completions (eg lemma names) that come from Isabelle through PIDE are not yet there ... you'll have to press CTRL-B (or whatever shortcut you have for auto-completion), to also make these completions appear. > Another problem with the completion mechanism is that a completion > list > sometimes pops up when you don’t need it (typically after entering a > quotation mark), and then you cannot navigate the cursor up or down. I think you can configure this in etc/symbols. The one on quotation marks was introduced to remember the user that cartouches should be used where possible, instead of quots. -- Peter

**Follow-Ups**:**Re: [isabelle] Another newbie question...case-based proofs***From:*Wolfgang Jeltsch

**References**:**[isabelle] Another newbie question...case-based proofs***From:*John F. Hughes

**Re: [isabelle] Another newbie question...case-based proofs***From:*Thomas Sewell

**Re: [isabelle] Another newbie question...case-based proofs***From:*Nagashima, Yutaka

**Re: [isabelle] Another newbie question...case-based proofs***From:*Peter Lammich

**Re: [isabelle] Another newbie question...case-based proofs***From:*Christian Sternagel

**Re: [isabelle] Another newbie question...case-based proofs***From:*Wolfgang Jeltsch

- Previous by Date: Re: [isabelle] Another newbie question...case-based proofs
- Next by Date: [isabelle] LSFA 2019 - Second Call for papers
- Previous by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Next by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Cl-isabelle-users March 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list