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



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.