Re: [isabelle] Isabelle and Vim (was: Re: Another newbie proofs)

> On 5. Apr 2019, at 13:45, Wolfgang Jeltsch <wolfgang-it at> wrote:
> Am Freitag, den 05.04.2019, 12:21 +0200 schrieb Makarius:
>> On 12/03/2019 17:15, Wolfgang Jeltsch wrote:
>>> By the way, have there been any attempts so far to integrate
>>> Isabelle into Vim?
>> No, Isabelle is moving in the opposite direction.
> In what respect is Isabelle moving away from Vim?

Away from these old single-threaded text editor towards the glorious Prover-IDE infrastructure.

> I like Vim particularly for its efficient editing capabilities, things
> like jumping to the matching bracket or deleting everything enclosed by
> the quotation marks to the left and right of the cursor, all of which
> doesn’t involve complicated key combinations. I guess the goal is not to
> make Isabelle editing less efficient.
> So what is it that is considered bad about Vim and is more and more
> avoided by Isabelle?

Using your keyboard instead of the mouse ;-)

I am using emacs to edit theory file (with semantic highlighting provided by the Isabelle/VSCode-server), instead of Isabelle/jEdit. Because Isabelle/jEdit crashes around 3 times a day when I use it [1]. My emacs plugin is definitely far from being polished, but it does not crash and it it works with spacemacs if you want to try it out.


[1] I am not claiming that I am using Isabelle in the standard way.

> All the best,
> Wolfgang

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