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

categorize settings #212

Merged
merged 1 commit into from
Jan 22, 2023
Merged

categorize settings #212

merged 1 commit into from
Jan 22, 2023

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jan 22, 2023

We group settings into related categories.

ejgallego
ejgallego reviewed Jan 22, 2023
View reviewed changes
editor/code/package.json Outdated Show resolved Hide resolved
ejgallego
ejgallego reviewed Jan 22, 2023
View reviewed changes
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.

Nice! Some suggestions in comments.

editor/code/package.json Outdated Show resolved Hide resolved
editor/code/package.json Outdated Show resolved Hide resolved
editor/code/package.json Outdated Show resolved Hide resolved
@ejgallego ejgallego added this to the 0.1.4 milestone Jan 22, 2023
@Alizter Alizter force-pushed the ps/rr/categorize_settings branch 2 times, most recently from 53b71cf to 049e486 Compare January 22, 2023 18:19
@Alizter
Copy link
Collaborator Author

Alizter commented Jan 22, 2023

image

@Alizter
Copy link
Collaborator Author

Alizter commented Jan 22, 2023

@ejgallego I added a changelog.

@ejgallego
Copy link
Owner

How do I get to test this? I can't see where the hierarchy appears.

@Alizter
Copy link
Collaborator Author

Alizter commented Jan 22, 2023 •
edited
Loading

@ejgallego In the settings window under extensions. You might need to reload vscode at least twice.

ejgallego
ejgallego approved these changes Jan 22, 2023
View reviewed changes
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 this is great!

ejgallego
ejgallego reviewed Jan 22, 2023
View reviewed changes
editor/code/package.json Outdated
@@ -173,5 +191,11 @@
"typecheck": "tsc -b",
"compile": "npm run esbuild",
"watch": "npm run esbuild -- --watch"
},
"__metadata": {
Copy link
Owner

Choose a reason for hiding this comment

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

Umm, still this keeps appearing here, but it should not, right?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It's from make ts-fmt. It is quite annoying that compiling the project using make extension messes up all the formatting meaning I have to do make ts-fmt afterwards too, and that adds random crap here.

Copy link
Owner

Choose a reason for hiding this comment

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

I don't see any of that; but again you should never do make extension or make ts-fmt if you have vscode open.

I'd bet what you see here is a race between some watch target in vscode with some extensions you are using.

Copy link
Owner

Choose a reason for hiding this comment

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

BTW there is not way that make extension could modify any file in the source tree.

@ejgallego
Copy link
Owner

@ejgallego In the settings window under extensions. You might need to reload vscode at least twice.

Ok got it, turns out you need to make the setting window large enough.

@Alizter
categorize settings
bf2b9dc 
<!-- ps-id: c242dc91-93ae-49ff-b4f7-e7fac9627f53 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter merged commit bdf2610 into ejgallego:main Jan 22, 2023
@Alizter Alizter deleted the ps/rr/categorize_settings branch January 22, 2023 20:22
@ejgallego ejgallego mentioned this pull request Jan 29, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
e05654b 
CHANGES:

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

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - Press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and extended
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
6554f83 
CHANGES:

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

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - You can press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and "extended"
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jan 29, 2023
@ejgallego
[new release] coq-lsp (0.1.4+v8.16)
1b58197 
CHANGES:

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

 - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184)
 - The keybinding alt+enter in VSCode is now correctly scoped to be
   only active on Coq files (@artagnon, ejgallego/coq-lsp#188)
 - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197)
 - The info view is now script enabled and does client-side
   rendering. It is also now bundled with esbuild as part of the build
   process (@artagnon, @ejgallego, ejgallego/coq-lsp#171)
 - The no-op `--std` argument to the `coq-lsp` binary has been
   removed, beware of your setup in the extension settings
   (@ejgallego, ejgallego/coq-lsp#208)
 - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212)
 - `GoalAnswer`s now include the proof "stack" and better hypothesis
   information, changes are compatible with 0.1.3 `GoalAnswer` version
   (@ejgallego, ejgallego/coq-lsp#237)
 - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242,
   fixes ejgallego/coq-lsp#224)
 - In `_CoqProject`, `-impredicative-set` is now parsed correctly
   (@artagnon, ejgallego/coq-lsp#241)
 - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223)
 - `debug` option in the client / protocol that will enable Coq's backtraces
   (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248)
 - Full document stats are now correctly computed on checking
   resumption, still cached sentences will display the cached timing
   tho (@ejgallego, ejgallego/coq-lsp#257)
 - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260)
 - `_CoqProject` file is now detected using LSP client `rootPath`
   (@ejgallego, ejgallego/coq-lsp#261)
 - You can press `\` to trigger Unicode completion by the server. This
   behavior is configurable, with "off", "regular", and "extended"
   settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees
No one assigned
Labels
kind: enhancement New feature or request kind: redesign part: client (VSCode)
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.4
Development

Successfully merging this pull request may close these issues.
2 participants
@Alizter @ejgallego