search

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
25 stars 5 forks source link

Option to not generate HTML output #47

Closed m-fleury closed 2 years ago

m-fleury commented 3 years ago

There is now an option to generate text output instead of HTML output. This is not relevant for emacs, but is important for vim (@ThreeFx).

You need to pass the option "vscode_html_output=false" to Isabelle's VSCode server, i.e.,

"-o" "vscode_html_output=false"

Somewhere like https://github.com/ThreeFx/isabelle-lsp/blob/main/main.go#L145

ThreeFx commented 3 years ago

Cool, thanks! I'll rebase on your fork then, and see if I have time this week(end) to find some starting points for code action integration.

EDIT: Ah for reasons (AutoCorres) I'm stuck with Isabelle2020. I'll use that locally, but develop on master. It should :TM: be easy to backport the code action integration once it's done.

m-fleury commented 3 years ago

I forgot one location. It should not make a difference for you: the code is only called if you send a PIDE/set_message_margin message to resize the output and state buffer.