[ refactor ] IDE protocol as a separate module hierarchy #2171
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
Added 3 modules: Protocol.{Hex, IDE, SExp}
Prepare a stub package file so that we could install the protocol
messages + (de)serialisation separately from idris2api
gallais
added
the
event: IDM 2021/12
ohad
pushed a commit
to ohad/idris2-mode-1
that referenced
this pull request
Dec 8, 2021
added 2 commits
December 8, 2021 19:04
Based on [PR#11](idris-community/idris2-mode#11) which supports the new IDE protocol
ohad
pushed a commit
to ohad/idris-mode
that referenced
this pull request
Dec 8, 2021
Adds minor protocol version support See idris2 [PR#2171](idris-lang/Idris2#2171 new spec for [`Bounds`](https://github.com/idris-lang/Idris2/blob/dd8914f627604461632bb530cb734014a47f505f/src/Libraries/Text/Bounded.idr#L9-L16)
added 5 commits
December 9, 2021 08:25
Another breaking change: when we send the file context inside a warning, it is now sent with the `Bounds` convention
for `MetaVarLemma` and `IdrisVersion`
Result is outstanding because it is ambiguous
gallais
reviewed
Dec 13, 2021
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: G. Allais <[email protected]>
|
(If you go to the files tab you can add all the suggestions to a single batch and |
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: G. Allais <[email protected]>
gallais
changed the title
|
🚀 |
gallais
pushed a commit
to idris-community/idris2-mode
that referenced
this pull request
Dec 19, 2021
#11) * Update semantic highlighting code in line with the update IDE protocol See idris2 [PR#2171](idris-lang/Idris2#2171 new spec for [`Bounds`](https://github.com/idris-lang/Idris2/blob/dd8914f627604461632bb530cb734014a47f505f/src/Libraries/Text/Bounded.idr#L9-L16) * Fix off-by-1 error Co-authored-by: Ohad Kammar <[email protected]>
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.
Much left to do:
New message types:
SExp'sBreaking changes to the protocol:
Bounds, and this change would breaks, say, emacs's idris2-mode.We updated the following IDE protocol clients (currently draft PR until this one is merged):