Re: [isabelle] Isabelle and Vim

Hi Mathias,

I am not completely sure, whether I have the same issue (I did not relate it to hovering).
However, the slowness of prettify-symbols seems to be related to a lot of theory files, even if they are not opened for viewing or editing.
So I think, your proposed solution might fix my problem.

And thank you for the overview plugin! I will try it sometime in the future when I upgrade my theories from Isabelle 2017.


On 8. Apr 2019, at 11:20, Mathias Fleury <mathias.fleury12 at<mailto:mathias.fleury12 at>> wrote:

Hi all,

On 5. Apr 2019, at 16:23, Berg, Nils Erik <nils.jaehnig at<mailto:nils.jaehnig at>> wrote:

Hi Wolfgang,

I really recommend you try VSCode with the Vim plugin.
I only use basic features of Vim, so I can't speak about more advanced functionality.

In general, Isabelle in VSCode is quite good. Sometimes I miss something (or did not search long enough) like e.g. the search functionality,

an overview over the status of all the theory.

I have a patch to add the overview (attached the version for Isabelle2018*). It requires a change in the plugin and in the Isabelle server. Basically apply the patch in the Isabelle repo, compile and install the plugin, and run VSCode with it.

For those things, I switch to jedit.

My only pain point is currently that the pretty symbols plugin is sometimes very slow.

Out of curiosity, are you impacted by I opened that issue and decided some times later that the plugin was too buggy to be usable, especially on large files.


* I have a patch for the Isabelle-dev, but I have not heard back from Makarius yet.


But all in all very usable and you can edit Vim-style.


On 5. Apr 2019, at 16:15, Wolfgang Jeltsch <wolfgang-it at<mailto:wolfgang-it at>> wrote:

Am Freitag, den 05.04.2019, 15:14 +0200 schrieb Makarius:
On 05/04/2019 13:45, Wolfgang Jeltsch wrote:

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.

Such basic editing facilities can still be added to the jEdit text
editor, by working with the (rather small) developer group at
SourceForge. I do this occasionally, but only for really important
things (like updates to HiDPI displays, updates to Java 11 etc.).

I doubt that Vim-style editing can be reasonably added to any
“mainstream” editor or IDE, as these tools typically don’t distinguish
between different modes. Vim’s distinction between normal mode (for
commands) and insert mode (for entering text) is crucial, as it allows
commands to be entered mostly by single key presses, avoiding things
like Ctrl + Shift + ….

Isabelle/PIDE is not so much a text editor, than a semantic IDE.
Editing is important, but not the key thing. For example, when I use
IntelliJ IDEA, I hardly know (and hardly care) about its editing
functions, and still manage to work on large Scala projects smoothly.

Before I started using Vim, I also didn’t care so much about editing
features. Now that I’ve realized how efficient your editing can be with
Vim, it can get quite annoying for me not to have such features. The
broad acceptance of more “mainstream” editors may have to do with the
fact that many people never got into advanced editing so much and thus
don’t know what they miss. Even many Vim users have an editing style
that stays way behind what is possible with Vim.

All the best,

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