Re: [isabelle] Another newbie proofs

On 05/04/2019 13:31, Mathias Fleury wrote:
> As long as Isabelle supports the language server protocol, it is possible to make vim interact with Isabelle (with some limitations; e.g., there are no colours in the equivalent of the 'buffer+output buffer'). However, the integration requires some work. I don't know anything about the internals of vim, but, at least in emacs, the lack of multithreading is an issue.

I would say that is rather theoretical. A really working Prover IDE
requires a lot of polishing and finishing beyond such standardized (and
limited) protocols.

> Otherwise, VSCode probably has a mode with vim keybindings.

It has one, but vim users have told me that it is not very serious. I
also see a vi mode in IntelliJ IDEA, but cannot say anything about its

Generally, one needs to understand that Isabelle came out of an Emacs
environment, but in the past 7 years that has been lost its relevance.
Since 4.5 years there is no way to get back to it.

Vi never had a role in the Isabelle community. It is a plain text
editor, not the basis of a multithreaded IDE.


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