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

Color changes for light color themes. #539

Merged
merged 3 commits into from
Sep 25, 2023
Merged

Conversation

bhaktishh
Copy link
Collaborator

@bhaktishh bhaktishh commented Aug 16, 2023

as per #532 .
Screenshot 2023-08-17 at 12 19 20 AM

@Alizter
Copy link
Collaborator

Alizter commented Aug 16, 2023

@bhaktishh Can you post a screenshot of how it looks?

@bhaktishh
Copy link
Collaborator Author

@bhaktishh Can you post a screenshot of how it looks?

sure, updated.

Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot @bhaktishh !

@corwin-of-amber , does this make sense to you?

Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, @bhaktishh , would you mind adding a CHANGES entry so the imrprovement reaches the changelog?

@bhaktishh
Copy link
Collaborator Author

@ejgallego let me know if that works!

Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@ejgallego ejgallego merged commit b63e22d into ejgallego:main Sep 25, 2023
11 checks passed
@ejgallego ejgallego linked an issue Sep 29, 2023 that may be closed by this pull request
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Oct 25, 2023
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Oct 25, 2023
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Oct 25, 2023
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Feb 5, 2024
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Feb 6, 2024
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

-------------------------------

 - Update VSCode client dependencies, should bring some performance
   improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530)
 - Update goal display colors for light mode so they are actually
   readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532)
 - Added link to Python coq-lsp client by Pedro Carrot and Nuno
   Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536)
 - Properly concatenate warnings from _CoqProject (@ejgallego,
   reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540)
 - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
   parsing problem with extra fields in their requests (@ejgallego,
   ejgallego/coq-lsp#547, reported by @Zimmi48)
 - `fcc` now understands the `--coqlib`, `--coqcorelib`,
   `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555)
 - Describe findlib status in `Workspace.describe`, which is printed
   in the output windows (@ejgallego, ejgallego/coq-lsp#556)
 - `coq-lsp` plugin loader will now be strict in case of a plugin
   failure, the previous loose behavior was more convenient for the
   early releases, but it doesn't make sense now and made things
   pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557)
 - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559)
 - Recognize `Goal` and `Definition $id : ... .` as proof starters
   (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548)
 - Provide basic notation information on hover. This is intended for
   people to build their own more refined notation feedback systems
   (@ejgallego, ejgallego/coq-lsp#562)
 - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562)
 - Updated LSP and JS client libs, notably to vscode-languageclient 9
   (@ejgallego, ejgallego/coq-lsp#565)
 - Implement a LIFO document scheduler, this is heavier in the
   background as more documents will be checked, but provides a few
   usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by
   Ali Caglayan)
 - New lexical qed detection error recovery rule; this makes a very
   large usability difference in practice when editing inside proofs.
   (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33)
 - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
   @CohenCyril, ejgallego/coq-lsp#572, via
   coq-community/coq-nix-toolbox#164 )
 - Support for `-rifrom` in `_CoqProject` and in command line
   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
   (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579)
 - Export Query Goals API in VSCode client; this way other extensions
   can implement their own commands that query Coq goals (@amblafont,
   @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558)
 - New `pretac` field for preprocessing of goals with a tactic using
   speculative execution, this is experimental for now (@amblafont,
   @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558)
 - Implement `textDocument/selectionRange` request, that will return
   the range of the Coq sentence underlying the cursor. In VSCode,
   this is triggered by the "Expand Selection" command. The
   implementation is partial: we only take into account the first
   position, and we only return a single range (Coq sentence) without
   parents. (@ejgallego, ejgallego/coq-lsp#582)
 - Be more robust to mixed-separator windows paths in workspace
   detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569)
 - Adjust printing breaks in error and message panels (@ejgallego,
   @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Fixed light color in the goal panel
3 participants