-
Notifications
You must be signed in to change notification settings - Fork 35
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
Added required support for ViZX Extension #469
Conversation
let vizx = extensions.getExtension("inQWIRE.vizx"); | ||
if (vizx?.isActive) { | ||
commands.executeCommand("vizx.lspRender", goals); | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me as a prototype, will merge so you can continue your testing.
I propose we indeed move towards a registration mechanism like done in most parts of VSCode, so eventually we can replace this code with your extension doing in activation:
let coq-lsp = extensions.getExtension("coq-lsp").?API_v1
coq-lsp.registerGoalProcessorString((goals) => lspRender(goals))
We may need a bit different API once we need to properly manage the UI resources both extensions handle, but that should be a good start.
Couple of comments for further PRs:
|
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
CHANGES: ----------------------------- - New command line compiler `fcc`. `fcc` allows to access most features of `coq-lsp` without the need for a command line client, and it has been designed to be extensible and machine-friendly (@ejgallego, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#438, reported by David Ilcinkas) - Fix "Error message browser becomes non-visible when there are many goals" by using a fixed-position separated error display (@TDiazT, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#470) - New command line argument `--idle-delay=$secs` that controls how much an idle server will sleep before going back to request processing. Default setting is `0.1`, using more aggressive settings like `0.01` can decrease latency of requests by ~4x (@ejgallego, @HazardousPeach, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#506) - Limit the number of messages displayed in the goal window to 101, as to workaround slow render of Coq's pretty printing format. This is an issue for example in Search where we can get thousand of results. We also speed up the rendering a bit by not hashing twice, and fix a parameter-passing bug. (@ejgallego, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ViZX can be found here. I just added code to execute a ViZX command when the extension is active; the goal is to enrich some textual goal display with a visualization; this command will simply open a webview with the visualization. ViZX has to be installed and active for the command to be executed; the goals object is the only information passed to ViZX.