Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

isabelle vscode_server does not support vscode_html_output #3

Open
christiankissig opened this issue Oct 18, 2023 · 1 comment · May be fixed by #4
Open

isabelle vscode_server does not support vscode_html_output #3

christiankissig opened this issue Oct 18, 2023 · 1 comment · May be fixed by #4

Comments

@christiankissig
Copy link

coc-isabelle defaults to setting the vscode_html_output option to false here https://github.com/ThreeFx/coc-isabelle/blob/main/src/index.ts#L23

    if (!config.get<boolean>('useHtmlOutput', false)) {
        extraArgs.push('-o', 'vscode_html_output=false')
    }

but the VSCode extension of Isabelle doesn't support the option

https://github.com/seL4/isabelle/blob/master/src/Tools/VSCode/etc/options

so that the command line, the plugin composes, breaks with this output

❯ isabelle vscode_server -o vscode_html_output=false
Content-Length: 176

{"jsonrpc":"2.0","method":"window/showMessage","params":{"type":1,"message":"Unknown option \"vscode_html_output\"\nThe error(s) above occurred in command-line option \"-o\""}}*** Unknown option "vscode_html_output"
*** The error(s) above occurred in command-line option "-o"

I'm using

❯ isabelle version
Isabelle2023

What am I missing?

@Treeniks
Copy link

Treeniks commented Nov 5, 2023

From what I understand, this repository does not use the original Isabelle VSCode language server, but instead the modified language server of isabelle-emacs. That one at least does have a vscode_html_output option as well as the PIDE/progress and PIDE/progress_request messages which are also missing otherwise.

@christiankissig christiankissig linked a pull request Nov 8, 2023 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants