Re: [isabelle] Another newbie question...case-based proofs



For auto completion, there is an option somewhere in preferences that make
it faster. And sorry could not remember where exactly (emailing from my
phone).

Best wishes

On Tue, Mar 12, 2019 at 4:22 PM Wolfgang Jeltsch <wolfgang-it at jeltsch.info>
wrote:

> Am Dienstag, den 12.03.2019, 09:24 +0100 schrieb Christian Sternagel:
> > In this session I never even opened either the output or state panels
> > (neither did I use "apply", for that matter).
> >
> > Instead I told students to start from a proof attempt along the lines
> > of
> >
> >   by (induction ...) auto
> >
> > and then consult the resulting error message (click on the squiggly
> > underline) for what they might be missing.
>
> This means they have to use the mouse and explicitly close error message
> windows. Such a workflow would be pretty uncomfortable for me.
>
> 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.
>
> Currently you have to wait a bit before you can complete macros for
> symbols with the tab key. That’s very annoying if you are used to type
> fluently, because you have to make artificial breaks in your typing. In
> order to not delay your typing more than necessary, you have the
> incentive to make those breaks as short as possible, but this may lead
> to too short a break, with the consequence that you have to delete
> several characters and start over again.
>
> 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.
>
> Could this situation be improved, or are these things too much wired
> into jEdit?
>
> By the way, have there been any attempts so far to integrate Isabelle
> into Vim?
>
> All the best,
> Wolfgang
>
>



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