categorize settings #212
Merged
categorize settings #212
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ejgallego
reviewed
Jan 22, 2023
ejgallego
reviewed
Jan 22, 2023
ejgallego
added
kind: enhancement
Alizter
force-pushed
the
ps/rr/categorize_settings
branch
2 times, most recently
from
53b71cf to
049e486
Compare
|
|
Alizter
force-pushed
the
ps/rr/categorize_settings
branch
from
049e486 to
e97fd1f
Compare
|
@ejgallego I added a changelog. |
|
How do I get to test this? I can't see where the hierarchy appears. |
|
@ejgallego In the settings window under extensions. You might need to reload vscode at least twice. |
ejgallego
reviewed
Jan 22, 2023
editor/code/package.json
Outdated
| @@ -173,5 +191,11 @@ | |||
| "typecheck": "tsc -b", | |||
| "compile": "npm run esbuild", | |||
| "watch": "npm run esbuild -- --watch" | |||
| }, | |||
| "__metadata": { | |||
There was a problem hiding this comment.
Umm, still this keeps appearing here, but it should not, right?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
BTW there is not way that make extension could modify any file in the source tree.
Ok got it, turns out you need to make the setting window large enough. |
<!-- ps-id: c242dc91-93ae-49ff-b4f7-e7fac9627f53 --> Signed-off-by: Ali Caglayan <[email protected]>
Alizter
force-pushed
the
ps/rr/categorize_settings
branch
from
e97fd1f to
bf2b9dc
Compare
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jan 29, 2023
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
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
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We group settings into related categories.