Stream: General

Topic: vscode_html_output

view this post on Zulip George Granberry (Sep 04 2024 at 10:27):

So in previous versions of Isabelle, there was an option for "vscode_html_output" but I'm not finding that in Isabelle2024. Is there a similar option under a different name?

view this post on Zulip Mathias Fleury (Sep 04 2024 at 12:00):

isn't it on by default now?

view this post on Zulip George Granberry (Sep 04 2024 at 13:06):

Yeah but I want to turn it off haha

view this post on Zulip Mathias Fleury (Sep 04 2024 at 13:12):

I have a fork where it still happens to be in https://github.com/m-fleury/isabelle-emacs/, but I have not tried VSCode in a while (the only difference to the standard Isabelle is that the LSP server has some more features)

view this post on Zulip George Granberry (Sep 04 2024 at 13:14):

I think we have similar use cases. I'm trying to get it working in a neovim setup :laughing:

view this post on Zulip George Granberry (Sep 04 2024 at 13:16):

Thanks for the branch, I'll get this setup on my machine

view this post on Zulip Mathias Fleury (Sep 04 2024 at 13:16):

Yeah I kept it because someone else asked for vim: https://github.com/m-fleury/isabelle-emacs/issues/47

view this post on Zulip Mathias Fleury (Sep 04 2024 at 13:17):

The repo https://github.com/ThreeFx/isabelle.vim

view this post on Zulip Mathias Fleury (Sep 04 2024 at 13:18):

seems to target neovim too, but I have never tried it

view this post on Zulip Mathias Fleury (Sep 04 2024 at 13:19):

And I cannot tell if it still works with the most recent neovim version

view this post on Zulip George Granberry (Sep 04 2024 at 13:40):

Works like a charm, thanks so much!

view this post on Zulip Fabian Huch (Sep 04 2024 at 15:23):

There is another neovim implementation, with substantial changes to the Isabelle Language Server: https://github.com/Treeniks/isabelle-lsp.nvim

view this post on Zulip Mathias Fleury (Sep 04 2024 at 19:26):

Yeah, I have given up getting my changes upstreamed

view this post on Zulip Mathias Fleury (Sep 04 2024 at 19:27):

Do you know if Treeniks bachelor thesis is already written? because it looks like I should really read it (I assume he is one of your students)

view this post on Zulip Fabian Huch (Sep 05 2024 at 08:15):

Mathias Fleury said:

Do you know if Treeniks bachelor thesis is already written? because it looks like I should really read it (I assume he is one of your students)

Yes, it should be available through our university library in time -- I'll ask him to put it on our website as well.

Last updated: Dec 21 2024 at 12:33 UTC