[coq] [fleche] Unicode Support #200
Merged
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
force-pushed
the
unicode_pos
branch
from
2868777 to
7aa5160
Compare
ejgallego
added
kind: enhancement
ejgallego
force-pushed
the
unicode_pos
branch
from
7aa5160 to
c93dff0
Compare
ejgallego
commented
Jan 19, 2023
ejgallego
force-pushed
the
unicode_pos
branch
5 times, most recently
from
9549f57 to
e6b8d4e
Compare
ejgallego
force-pushed
the
unicode_pos
branch
5 times, most recently
from
c2b1a37 to
f467687
Compare
ejgallego
changed the title
ejgallego
force-pushed
the
unicode_pos
branch
from
f467687 to
52b0fc8
Compare
ejgallego
force-pushed
the
unicode_pos
branch
2 times, most recently
from
07cdb97 to
3ed7625
Compare
Alizter
reviewed
Jan 19, 2023
Alizter
approved these changes
Jan 19, 2023
ejgallego
force-pushed
the
unicode_pos
branch
from
3ed7625 to
186cb26
Compare
We enforce a stricter separation between `Range.t` and `Loc.t`, with Flèche not using `Loc.t` anymore, and `Range.t` being in unicode character positions. To achieve this we need to convert all the positions coming from Coq; we do this in a principled way, but the whole business is often delicate. As we keep a position per sentence, this implies a `O(n)` number of conversions in total, where `n is the number of sentences; we could optimize that to be lazy, but it is unlikely to show in profiles as that is a pretty reasonably `O(.)` factor. Fixes #193 , fixes #197 .
|
@Alizter I think I'm happy with the code now; how did your testing go? |
ejgallego
force-pushed
the
unicode_pos
branch
from
0260a09 to
308ab27
Compare
We had some code duplication coming from #179, time to consolidate it.
ejgallego
force-pushed
the
unicode_pos
branch
from
70f5606 to
9e148ff
Compare
|
@ejgallego my issues have been resolved. |
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 enforce a stricter separation between
Range.tandLoc.t, withFlèche not using
Loc.tanymore, andRange.tbeing in unicodecharacter positions.
To achieve this we need to convert all the positions coming from Coq;
we do this in a principled way, but the whole business is often
delicate.
As we keep a position per sentence, this implies a
O(n)number ofconversions in total, where
n is the number of sentences; we could optimize that to be lazy, but it is unlikely to show in profiles as that is a pretty reasonablyO(.)` factor.Fixes #193 , fixes #197 .