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.

Sign up for GitHub

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

Jump to bottom

[goal printing] Use jsCoq goal printing code #96

Closed
ejgallego opened this issue Dec 16, 2022 · 1 comment · Fixed by #143, #290, ocaml/opam-repository#23390 or ocaml/opam-repository#23614
Closed

[goal printing] Use jsCoq goal printing code #96

ejgallego opened this issue Dec 16, 2022 · 1 comment · Fixed by #143, #290, ocaml/opam-repository#23390 or ocaml/opam-repository#23614
Assignees
@artagnon
Labels
part: client (VSCode)
Milestone
0.1.6

Comments

@ejgallego
Copy link
Owner

Current goal printing is very basic and doesn't look good at all; in particular we didn't set indentation and margins on, also there is no coloring.

Best way to fix this is to use jsCoq's Pp.t -> Html routine (https://github.com/jscoq/jscoq/blob/2a60fd083b6b09cbe19f750f31a877740d140ea2/frontend/classic/js/format-pprint.js) , which is well-tested and provides some nice features.
@ejgallego ejgallego added this to the 0.1.1 milestone Dec 16, 2022
@ejgallego ejgallego modified the milestones: 0.1.1, 0.1.2 Dec 22, 2022
@ejgallego ejgallego modified the milestones: 0.1.2, 0.1.3 Jan 5, 2023
@ejgallego ejgallego modified the milestones: 0.1.3, 0.1.4 Jan 13, 2023
@ejgallego ejgallego modified the milestones: 0.1.4, 0.1.5 Jan 23, 2023
@Alizter Alizter moved this to Todo in coq-lsp roadmap Jan 29, 2023
@ejgallego ejgallego modified the milestones: 0.1.5, 0.1.6 Feb 7, 2023
ejgallego added a commit that referenced this issue Feb 15, 2023
@ejgallego
Merge pull request #143 from artagnon/goal-prettify
401444a 
goals: lay foundation for pretty-printing goals (#96)
@ejgallego
Copy link
Owner Author

Fixed by #143

@github-project-automation github-project-automation bot moved this from Todo to Done in coq-lsp roadmap Feb 15, 2023
This was linked to pull requests Feb 15, 2023
goals: lay foundation for pretty-printing goals (#96) #143
Merged
[goals] Adapt jsCoq goal printing code to VS Code / React #290
Merged
@ejgallego ejgallego mentioned this issue Feb 22, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 22, 2023
@ejgallego
[new release] coq-lsp (0.1.6+8.16)
673cf97 
CHANGES:

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

 - The info / goal view now uses jsCoq's client-side rendering, with
   better highlighting and layout rendering (@artagnon, @ejgallego,
   ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#96)
 - Printing method is now configurable by the user (@ejgallego, ejgallego/coq-lsp#143,
   fixes ejgallego/coq-lsp#321)
 - Trigger completion on quote char "'" (@ejgallego, ejgallego/coq-lsp#350)
 - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/coq-lsp#357)
 - New request `coq/getDocument` to get serialized full document
   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
   (@ejgallego, ejgallego/coq-lsp#350)
 - Auto-ignore Coq object files; can be disabled in config
   (@ejgallego, ejgallego/coq-lsp#365)
 - Support workspaces with multiple roots, this is very useful for
   projects that contain several `_CoqProject` files in different
   directories (@ejgallego, ejgallego/coq-lsp#374)
 - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/coq-lsp#377,
   cc ejgallego/coq-lsp#209)
 - Fix bug that made the server not exit on `exit` LSP notification
   (@artagnon, @ejgallego, ejgallego/coq-lsp#375, fixes ejgallego/coq-lsp#230)
 - Lay the foundation for server tests (@artagnon, ejgallego/coq-lsp#356)
 - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/coq-lsp#129)
 - Print abbreviations on hover (@ejgallego, ejgallego/coq-lsp#384)
 - Print hover types without parenthesis (@ejgallego, ejgallego/coq-lsp#384)
 - Parse identifiers with dot for hover and jump to definition
   (@ejallego, ejgallego/coq-lsp#385)
 - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter,
   ejgallego/coq-lsp#383, fixes ejgallego/coq-lsp#273)
 - Fix typo on max_errors checking, this made coq-lsp stop on the
   number of total diagnostics, instead of only errors (@ejgallego,
   ejgallego/coq-lsp#386)
 - Hover symbol information: hypothesis names must shadow globals of
   the same name (@ejgallego, ejgallego/coq-lsp#391, fixes ejgallego/coq-lsp#388)
 - De-schedule document on didClose, otherwise the scheduler will keep
   trying to resume it if it didn't finish (@ejgallego, ejgallego/coq-lsp#392)
 - Hover symbol information: correctly handle identifiers before '.'
   and containing a quote (') themselves (@ejgallego, ejgallego/coq-lsp#393)
 - Add children entries to the table-of-contents (@ejgallego, ejgallego/coq-lsp#394)
 - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
   ejgallego/coq-lsp#395)
 - Add status bar button to toggle server run status (@ejgallego,
   @Alizter, ejgallego/coq-lsp#378, closes ejgallego/coq-lsp#209)
 - Support for `COQLIB` and `COQCORELIB` environment variables, added
   `--coqcorelib` command line argument (@ejgallego, ejgallego/coq-lsp#403)
 - Protocol infrastructure for code lenses (@ejgallego, ejgallego/coq-lsp#396)
 - Set binary more for protocol input / output (@ejgallego, ejgallego/coq-lsp#408)
 - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/coq-lsp#408)
 - Windows support (@ejgallego, @jim-portegies, ejgallego/coq-lsp#408)
 - Scroll active goal into view (@ejgallego, ejgallego/coq-lsp#410, fixes ejgallego/coq-lsp#381)
 - Server status icon will now react properly to fatal server errors
   (@ejgallego, reported by @Alizter, ejgallego/coq-lsp#411, fixes ejgallego/coq-lsp#399)
 - Info on memory and time is now disabled by default, new option
   `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/coq-lsp#412,
   fixes ejgallego/coq-lsp#398).
 - `coq-lsp` can now save `.vo` files for files opened in the
   editor. Use the new "Save to .vo" command, or the new protocol
   `coq/saveVo` request (@ejgallego, ejgallego/coq-lsp#417, fixes ejgallego/coq-lsp#339)
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 22, 2023
@ejgallego
[new release] coq-lsp (0.1.6+8.16)
53847ed 
CHANGES:

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

 - The info / goal view now uses jsCoq's client-side rendering, with
   better highlighting and layout rendering (@artagnon, @ejgallego,
   ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#96)
 - Printing method is now configurable by the user (@ejgallego, ejgallego/coq-lsp#143,
   fixes ejgallego/coq-lsp#321)
 - Trigger completion on quote char "'" (@ejgallego, ejgallego/coq-lsp#350)
 - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/coq-lsp#357)
 - New request `coq/getDocument` to get serialized full document
   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
   (@ejgallego, ejgallego/coq-lsp#350)
 - Auto-ignore Coq object files; can be disabled in config
   (@ejgallego, ejgallego/coq-lsp#365)
 - Support workspaces with multiple roots, this is very useful for
   projects that contain several `_CoqProject` files in different
   directories (@ejgallego, ejgallego/coq-lsp#374)
 - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/coq-lsp#377,
   cc ejgallego/coq-lsp#209)
 - Fix bug that made the server not exit on `exit` LSP notification
   (@artagnon, @ejgallego, ejgallego/coq-lsp#375, fixes ejgallego/coq-lsp#230)
 - Lay the foundation for server tests (@artagnon, ejgallego/coq-lsp#356)
 - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/coq-lsp#129)
 - Print abbreviations on hover (@ejgallego, ejgallego/coq-lsp#384)
 - Print hover types without parenthesis (@ejgallego, ejgallego/coq-lsp#384)
 - Parse identifiers with dot for hover and jump to definition
   (@ejallego, ejgallego/coq-lsp#385)
 - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter,
   ejgallego/coq-lsp#383, fixes ejgallego/coq-lsp#273)
 - Fix typo on max_errors checking, this made coq-lsp stop on the
   number of total diagnostics, instead of only errors (@ejgallego,
   ejgallego/coq-lsp#386)
 - Hover symbol information: hypothesis names must shadow globals of
   the same name (@ejgallego, ejgallego/coq-lsp#391, fixes ejgallego/coq-lsp#388)
 - De-schedule document on didClose, otherwise the scheduler will keep
   trying to resume it if it didn't finish (@ejgallego, ejgallego/coq-lsp#392)
 - Hover symbol information: correctly handle identifiers before '.'
   and containing a quote (') themselves (@ejgallego, ejgallego/coq-lsp#393)
 - Add children entries to the table-of-contents (@ejgallego, ejgallego/coq-lsp#394)
 - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
   ejgallego/coq-lsp#395)
 - Add status bar button to toggle server run status (@ejgallego,
   @Alizter, ejgallego/coq-lsp#378, closes ejgallego/coq-lsp#209)
 - Support for `COQLIB` and `COQCORELIB` environment variables, added
   `--coqcorelib` command line argument (@ejgallego, ejgallego/coq-lsp#403)
 - Protocol infrastructure for code lenses (@ejgallego, ejgallego/coq-lsp#396)
 - Set binary more for protocol input / output (@ejgallego, ejgallego/coq-lsp#408)
 - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/coq-lsp#408)
 - Windows support (@ejgallego, @jim-portegies, ejgallego/coq-lsp#408)
 - Scroll active goal into view (@ejgallego, ejgallego/coq-lsp#410, fixes ejgallego/coq-lsp#381)
 - Server status icon will now react properly to fatal server errors
   (@ejgallego, reported by @Alizter, ejgallego/coq-lsp#411, fixes ejgallego/coq-lsp#399)
 - Info on memory and time is now disabled by default, new option
   `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/coq-lsp#412,
   fixes ejgallego/coq-lsp#398).
 - `coq-lsp` can now save `.vo` files for files opened in the
   editor. Use the new "Save to .vo" command, or the new protocol
   `coq/saveVo` request (@ejgallego, ejgallego/coq-lsp#417, fixes ejgallego/coq-lsp#339)
@ejgallego ejgallego mentioned this issue Apr 3, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Apr 3, 2023
@ejgallego
[new release] coq-lsp (0.1.6.1+8.17)
f1962a2 
CHANGES:

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

 - The info / goal view now uses jsCoq's client-side rendering, with
   better highlighting and layout rendering (@artagnon, @ejgallego,
   ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#96)
 - Printing method is now configurable by the user (@ejgallego, ejgallego/coq-lsp#143,
   fixes ejgallego/coq-lsp#321)
 - Trigger completion on quote char "'" (@ejgallego, ejgallego/coq-lsp#350)
 - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/coq-lsp#357)
 - New request `coq/getDocument` to get serialized full document
   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
   (@ejgallego, ejgallego/coq-lsp#350)
 - Auto-ignore Coq object files; can be disabled in config
   (@ejgallego, ejgallego/coq-lsp#365)
 - Support workspaces with multiple roots, this is very useful for
   projects that contain several `_CoqProject` files in different
   directories (@ejgallego, ejgallego/coq-lsp#374)
 - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/coq-lsp#377,
   cc ejgallego/coq-lsp#209)
 - Fix bug that made the server not exit on `exit` LSP notification
   (@artagnon, @ejgallego, ejgallego/coq-lsp#375, fixes ejgallego/coq-lsp#230)
 - Lay the foundation for server tests (@artagnon, ejgallego/coq-lsp#356)
 - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/coq-lsp#129)
 - Print abbreviations on hover (@ejgallego, ejgallego/coq-lsp#384)
 - Print hover types without parenthesis (@ejgallego, ejgallego/coq-lsp#384)
 - Parse identifiers with dot for hover and jump to definition
   (@ejallego, ejgallego/coq-lsp#385)
 - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter,
   ejgallego/coq-lsp#383, fixes ejgallego/coq-lsp#273)
 - Fix typo on max_errors checking, this made coq-lsp stop on the
   number of total diagnostics, instead of only errors (@ejgallego,
   ejgallego/coq-lsp#386)
 - Hover symbol information: hypothesis names must shadow globals of
   the same name (@ejgallego, ejgallego/coq-lsp#391, fixes ejgallego/coq-lsp#388)
 - De-schedule document on didClose, otherwise the scheduler will keep
   trying to resume it if it didn't finish (@ejgallego, ejgallego/coq-lsp#392)
 - Hover symbol information: correctly handle identifiers before '.'
   and containing a quote (') themselves (@ejgallego, ejgallego/coq-lsp#393)
 - Add children entries to the table-of-contents (@ejgallego, ejgallego/coq-lsp#394)
 - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
   ejgallego/coq-lsp#395)
 - Add status bar button to toggle server run status (@ejgallego,
   @Alizter, ejgallego/coq-lsp#378, closes ejgallego/coq-lsp#209)
 - Support for `COQLIB` and `COQCORELIB` environment variables, added
   `--coqcorelib` command line argument (@ejgallego, ejgallego/coq-lsp#403)
 - Protocol infrastructure for code lenses (@ejgallego, ejgallego/coq-lsp#396)
 - Set binary mode for protocol input / output (@ejgallego, ejgallego/coq-lsp#408)
 - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/coq-lsp#408)
 - Windows support (@ejgallego, @jim-portegies, ejgallego/coq-lsp#408)
 - Scroll active goal into view (@ejgallego, ejgallego/coq-lsp#410, fixes ejgallego/coq-lsp#381)
 - Server status icon will now react properly to fatal server errors
   (@ejgallego, reported by @Alizter, ejgallego/coq-lsp#411, fixes ejgallego/coq-lsp#399)
 - Info on memory and time is now disabled by default, new option
   `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/coq-lsp#412,
   fixes ejgallego/coq-lsp#398).
 - `coq-lsp` can now save `.vo` files for files opened in the
   editor. Use the new "Save to .vo" command, or the new protocol
   `coq/saveVo` request (@ejgallego, ejgallego/coq-lsp#417, fixes ejgallego/coq-lsp#339)
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Apr 3, 2023
@ejgallego
[new release] coq-lsp (0.1.6.1+8.17)
3c26d05 
CHANGES:

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

 - The info / goal view now uses jsCoq's client-side rendering, with
   better highlighting and layout rendering (@artagnon, @ejgallego,
   ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#96)
 - Printing method is now configurable by the user (@ejgallego, ejgallego/coq-lsp#143,
   fixes ejgallego/coq-lsp#321)
 - Trigger completion on quote char "'" (@ejgallego, ejgallego/coq-lsp#350)
 - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/coq-lsp#357)
 - New request `coq/getDocument` to get serialized full document
   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
   (@ejgallego, ejgallego/coq-lsp#350)
 - Auto-ignore Coq object files; can be disabled in config
   (@ejgallego, ejgallego/coq-lsp#365)
 - Support workspaces with multiple roots, this is very useful for
   projects that contain several `_CoqProject` files in different
   directories (@ejgallego, ejgallego/coq-lsp#374)
 - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/coq-lsp#377,
   cc ejgallego/coq-lsp#209)
 - Fix bug that made the server not exit on `exit` LSP notification
   (@artagnon, @ejgallego, ejgallego/coq-lsp#375, fixes ejgallego/coq-lsp#230)
 - Lay the foundation for server tests (@artagnon, ejgallego/coq-lsp#356)
 - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/coq-lsp#129)
 - Print abbreviations on hover (@ejgallego, ejgallego/coq-lsp#384)
 - Print hover types without parenthesis (@ejgallego, ejgallego/coq-lsp#384)
 - Parse identifiers with dot for hover and jump to definition
   (@ejallego, ejgallego/coq-lsp#385)
 - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter,
   ejgallego/coq-lsp#383, fixes ejgallego/coq-lsp#273)
 - Fix typo on max_errors checking, this made coq-lsp stop on the
   number of total diagnostics, instead of only errors (@ejgallego,
   ejgallego/coq-lsp#386)
 - Hover symbol information: hypothesis names must shadow globals of
   the same name (@ejgallego, ejgallego/coq-lsp#391, fixes ejgallego/coq-lsp#388)
 - De-schedule document on didClose, otherwise the scheduler will keep
   trying to resume it if it didn't finish (@ejgallego, ejgallego/coq-lsp#392)
 - Hover symbol information: correctly handle identifiers before '.'
   and containing a quote (') themselves (@ejgallego, ejgallego/coq-lsp#393)
 - Add children entries to the table-of-contents (@ejgallego, ejgallego/coq-lsp#394)
 - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
   ejgallego/coq-lsp#395)
 - Add status bar button to toggle server run status (@ejgallego,
   @Alizter, ejgallego/coq-lsp#378, closes ejgallego/coq-lsp#209)
 - Support for `COQLIB` and `COQCORELIB` environment variables, added
   `--coqcorelib` command line argument (@ejgallego, ejgallego/coq-lsp#403)
 - Protocol infrastructure for code lenses (@ejgallego, ejgallego/coq-lsp#396)
 - Set binary mode for protocol input / output (@ejgallego, ejgallego/coq-lsp#408)
 - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/coq-lsp#408)
 - Windows support (@ejgallego, @jim-portegies, ejgallego/coq-lsp#408)
 - Scroll active goal into view (@ejgallego, ejgallego/coq-lsp#410, fixes ejgallego/coq-lsp#381)
 - Server status icon will now react properly to fatal server errors
   (@ejgallego, reported by @Alizter, ejgallego/coq-lsp#411, fixes ejgallego/coq-lsp#399)
 - Info on memory and time is now disabled by default, new option
   `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/coq-lsp#412,
   fixes ejgallego/coq-lsp#398).
 - `coq-lsp` can now save `.vo` files for files opened in the
   editor. Use the new "Save to .vo" command, or the new protocol
   `coq/saveVo` request (@ejgallego, ejgallego/coq-lsp#417, fixes ejgallego/coq-lsp#339)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@artagnon artagnon

Labels
part: client (VSCode)
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.6
2 participants
@artagnon @ejgallego