Update the TextMate grammar for rzk v0.11.0 - #78
Merged
Merged
Conversation
Highlight the new syntax: the #data command (the declared name as a type, with a uses clause as for #define), the match and into keywords and the eliminator clause, the branch arrows (Unicode and ASCII), and the lattice operations on cubes (sup, inf and their Unicode forms). Drop the pattern for brace parameters, removed in rzk v0.11.0. This also fixes a mis-highlighting: a single-line block comment containing a colon matched the brace-parameter pattern and was coloured as a parameter list instead of a comment (visible in the updated block-comments snapshot). The tope highlighting of paren-form shaped parameters is left to the term rules on purpose: a dedicated tope-bar rule cannot be told apart from the middle separator of a modal type <| m | A |>, and would restyle modal types in parameter position. New colorize assertions and a snapshot fixture cover #data, match (including an into motive), and the lattice operators.
The bracketing rule dates from the first modal-syntax PR; the modal syntax has since moved on (see #74), so the old spelling should not read as highlighted syntax. The tags and let mod/mod keywords are untouched.
With the modal-type bar dropped, the only bare | inside a paren parameter is the shape separator, so the tope-bar rule from the removed brace form is unambiguous and returns for (t : 2 | phi). Making it safe surfaced a latent bug, fixed here: the parameter-region opener let its identifier part cross a closing paren, so a non-parameter group before a later colon, as in #define vhead (xs : vec A (suc n)) : A opened a region at (suc n that spanned to the next line and mis-coloured it (a match-branch bar read as a tope bar). The identifier part now crosses only balanced paren groups, at any nesting depth via Oniguruma subexpression recursion, which keeps pair-pattern parameters like ( ( (a , b) , c) : A) styled. Colorize assertions cover the shaped-param tope, a nested pair pattern, and the non-spanning regression; the common fixture snapshot is unchanged.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
This PR updates the TextMate grammar to the rzk v0.11.0 syntax. TextMate colouring is the fallback while the language server has not yet checked a file (and the baseline below the semantic tokens), so the new constructs should not appear as plain text.
Added highlighting:
#datacommand: the command keyword colours as for#define, the declared name as a type, and theusesclause is supported;matchandintoas control keywords, and theeliminatorclause of a#databody;⇒/=>;sup/infbeside the other builtin functions, and⊔/⊓as operators.Removed: the pattern for brace parameters
{p : A | φ}, whose syntax rzk v0.11.0 removed (rzk-lang/rzk#304), and the bracketing of the old modal-type syntax<| m | A |>. This turned out to fix a mis-highlighting: a single-line block comment containing a colon, such as{- pretends to be #define foo : U := bar -}, matched the brace-parameter pattern and was coloured as a parameter list instead of a comment; the updatedblock-commentssnapshot shows the fix.With the modal-type bar gone, the tope of a paren-form shaped parameter
(t : 2 | φ)now colours the way the brace form used to (a tope bar followed by the tope): the only bare|left inside a parameter is the shape separator, so the rule is unambiguous. Making that safe surfaced a latent bug, also fixed here: the parameter-region opener let its identifier part cross a closing paren, so a non-parameter group before a later colon (as in(xs : vec A (suc n)) : A) opened a region spanning to the next line and mis-coloured it. The identifier part now only crosses balanced paren groups (pair patterns of any nesting depth, via Oniguruma subexpression recursion).Screenshots
Before semantic highlighting via Rzk language server:
With semantic highlighting: