Skip to content

Commit 55233c4

Browse files
fizrukfizruk
committed
Drop the highlighting of the old modal-type syntax <| m | A |>
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.
1 parent f6fddb0 commit 55233c4

5 files changed

Lines changed: 81 additions & 52 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Check [Keep a Changelog](http://keepachangelog.com/) for recommendations on how
1616
parameters `{p : A | φ}`). This also fixes a mis-highlighting: a
1717
single-line block comment containing a colon was coloured as a
1818
brace parameter instead of a comment.
19+
- Drop the highlighting of the old modal-type syntax `<| m | A |>`.
1920

2021
## v0.5.0 - 2026-07-14
2122

‎syntaxes/rzk.tmLanguage.json‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -160,10 +160,6 @@
160160
"name": "support.function.rzk",
161161
"match": "(?<=^|[.\\\\;,#\"\\]\\[)(}{><|\\s])mod(?=$|[.\\\\;,#\"\\]\\[)(}{><|\\s])"
162162
},
163-
{
164-
"name": "punctuation.definition.modtype.rzk",
165-
"match": "(<\\||\\|>)"
166-
},
167163
{
168164
"name": "invalid.rzk",
169165
"match": "\\$extract\\$"

‎syntaxes/rzk.tmLanguage.yml‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,8 +81,6 @@ repository:
8181
match: (?<=^|[.\\;,#"\]\[)(}{><|\s])in(?=$|[.\\;,#"\]\[)(}{><|\s])
8282
- name: support.function.rzk
8383
match: (?<=^|[.\\;,#"\]\[)(}{><|\s])mod(?=$|[.\\;,#"\]\[)(}{><|\s])
84-
- name: punctuation.definition.modtype.rzk
85-
match: (<\||\|>)
8684
- name: invalid.rzk
8785
match: \$extract\$
8886
- name: entity.name.tag.rzk

‎tests/colorize/new-constructs.rzk‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -29,12 +29,6 @@ let mod
2929
_id
3030
-- <-- entity.name.tag.rzk
3131

32-
-- Modal type bracketing
33-
<|
34-
-- <-- punctuation.definition.modtype.rzk
35-
|>
36-
-- <-- punctuation.definition.modtype.rzk
37-
3832
-- `Unit` type
3933
Unit
4034
-- <-- entity.name.type.rzk

‎tests/fixtures/modalities.rzk.snap‎

Lines changed: 80 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -69,23 +69,27 @@
6969
#^^ source.rzk
7070
# ^ source.rzk keyword.operator.rzk
7171
# ^ source.rzk
72-
# ^^ source.rzk punctuation.definition.modtype.rzk
72+
# ^ source.rzk keyword.operator.rzk
73+
# ^ source.rzk keyword.operator.rzk
7374
# ^ source.rzk
7475
# ^ source.rzk entity.name.tag.rzk
7576
# ^ source.rzk
7677
# ^ source.rzk keyword.operator.rzk
7778
# ^^^ source.rzk
78-
# ^^ source.rzk punctuation.definition.modtype.rzk
79+
# ^ source.rzk keyword.operator.rzk
80+
# ^ source.rzk keyword.operator.rzk
7981
# ^ source.rzk
8082
# ^ source.rzk keyword.operator.rzk
8183
# ^ source.rzk
82-
# ^^ source.rzk punctuation.definition.modtype.rzk
84+
# ^ source.rzk keyword.operator.rzk
85+
# ^ source.rzk keyword.operator.rzk
8386
# ^ source.rzk
8487
# ^ source.rzk entity.name.tag.rzk
8588
# ^ source.rzk
8689
# ^ source.rzk keyword.operator.rzk
8790
# ^^^ source.rzk
88-
# ^^ source.rzk punctuation.definition.modtype.rzk
91+
# ^ source.rzk keyword.operator.rzk
92+
# ^ source.rzk keyword.operator.rzk
8993
> :=
9094
#^^ source.rzk
9195
# ^^ source.rzk keyword.operator.rzk
@@ -136,21 +140,25 @@
136140
#^^ source.rzk
137141
# ^ source.rzk keyword.operator.rzk
138142
# ^ source.rzk
139-
# ^^ source.rzk punctuation.definition.modtype.rzk
143+
# ^ source.rzk keyword.operator.rzk
144+
# ^ source.rzk keyword.operator.rzk
140145
# ^ source.rzk
141146
# ^ source.rzk entity.name.tag.rzk
142147
# ^ source.rzk
143148
# ^ source.rzk keyword.operator.rzk
144149
# ^ source.rzk
145-
# ^^ source.rzk punctuation.definition.modtype.rzk
150+
# ^ source.rzk keyword.operator.rzk
151+
# ^ source.rzk keyword.operator.rzk
146152
# ^ source.rzk
147153
# ^ source.rzk entity.name.tag.rzk
148154
# ^ source.rzk
149155
# ^ source.rzk keyword.operator.rzk
150156
# ^^^ source.rzk
151-
# ^^ source.rzk punctuation.definition.modtype.rzk
157+
# ^ source.rzk keyword.operator.rzk
158+
# ^ source.rzk keyword.operator.rzk
152159
# ^ source.rzk
153-
# ^^ source.rzk punctuation.definition.modtype.rzk
160+
# ^ source.rzk keyword.operator.rzk
161+
# ^ source.rzk keyword.operator.rzk
154162
> :=
155163
#^^ source.rzk
156164
# ^^ source.rzk keyword.operator.rzk
@@ -196,23 +204,27 @@
196204
#^^ source.rzk
197205
# ^ source.rzk keyword.operator.rzk
198206
# ^ source.rzk
199-
# ^^ source.rzk punctuation.definition.modtype.rzk
207+
# ^ source.rzk keyword.operator.rzk
208+
# ^ source.rzk keyword.operator.rzk
200209
# ^ source.rzk
201210
# ^^ source.rzk entity.name.tag.rzk
202211
# ^ source.rzk
203212
# ^ source.rzk keyword.operator.rzk
204213
# ^^^ source.rzk
205-
# ^^ source.rzk punctuation.definition.modtype.rzk
214+
# ^ source.rzk keyword.operator.rzk
215+
# ^ source.rzk keyword.operator.rzk
206216
# ^ source.rzk
207217
# ^ source.rzk keyword.operator.rzk
208218
# ^ source.rzk
209-
# ^^ source.rzk punctuation.definition.modtype.rzk
219+
# ^ source.rzk keyword.operator.rzk
220+
# ^ source.rzk keyword.operator.rzk
210221
# ^ source.rzk
211222
# ^^ source.rzk entity.name.tag.rzk
212223
# ^ source.rzk
213224
# ^ source.rzk keyword.operator.rzk
214225
# ^^^ source.rzk
215-
# ^^ source.rzk punctuation.definition.modtype.rzk
226+
# ^ source.rzk keyword.operator.rzk
227+
# ^ source.rzk keyword.operator.rzk
216228
> :=
217229
#^^ source.rzk
218230
# ^^ source.rzk keyword.operator.rzk
@@ -254,21 +266,25 @@
254266
# ^ source.rzk
255267
# ^ source.rzk keyword.operator.colon.params.rzk
256268
# ^ source.rzk
257-
# ^^ source.rzk punctuation.definition.modtype.rzk
269+
# ^ source.rzk keyword.operator.rzk
270+
# ^ source.rzk keyword.operator.rzk
258271
# ^ source.rzk
259272
# ^^ source.rzk entity.name.tag.rzk
260273
# ^ source.rzk
261274
# ^ source.rzk keyword.operator.rzk
262275
# ^ source.rzk
263-
# ^^ source.rzk punctuation.definition.modtype.rzk
276+
# ^ source.rzk keyword.operator.rzk
277+
# ^ source.rzk keyword.operator.rzk
264278
# ^ source.rzk
265279
# ^^ source.rzk entity.name.tag.rzk
266280
# ^ source.rzk
267281
# ^ source.rzk keyword.operator.rzk
268282
# ^^^ source.rzk
269-
# ^^ source.rzk punctuation.definition.modtype.rzk
283+
# ^ source.rzk keyword.operator.rzk
284+
# ^ source.rzk keyword.operator.rzk
270285
# ^ source.rzk
271-
# ^^ source.rzk punctuation.definition.modtype.rzk
286+
# ^ source.rzk keyword.operator.rzk
287+
# ^ source.rzk keyword.operator.rzk
272288
# ^ source.rzk
273289
> : A
274290
#^^ source.rzk
@@ -323,13 +339,15 @@
323339
#^^ source.rzk
324340
# ^ source.rzk keyword.operator.rzk
325341
# ^ source.rzk
326-
# ^^ source.rzk punctuation.definition.modtype.rzk
342+
# ^ source.rzk keyword.operator.rzk
343+
# ^ source.rzk keyword.operator.rzk
327344
# ^ source.rzk
328345
# ^ source.rzk entity.name.tag.rzk
329346
# ^ source.rzk
330347
# ^ source.rzk keyword.operator.rzk
331348
# ^^^ source.rzk
332-
# ^^ source.rzk punctuation.definition.modtype.rzk
349+
# ^ source.rzk keyword.operator.rzk
350+
# ^ source.rzk keyword.operator.rzk
333351
> := mod ♯ x
334352
#^^ source.rzk
335353
# ^^ source.rzk keyword.operator.rzk
@@ -366,23 +384,27 @@
366384
#^^ source.rzk
367385
# ^ source.rzk keyword.operator.rzk
368386
# ^ source.rzk
369-
# ^^ source.rzk punctuation.definition.modtype.rzk
387+
# ^ source.rzk keyword.operator.rzk
388+
# ^ source.rzk keyword.operator.rzk
370389
# ^ source.rzk
371390
# ^ source.rzk entity.name.tag.rzk
372391
# ^ source.rzk
373392
# ^ source.rzk keyword.operator.rzk
374393
# ^^^ source.rzk
375-
# ^^ source.rzk punctuation.definition.modtype.rzk
394+
# ^ source.rzk keyword.operator.rzk
395+
# ^ source.rzk keyword.operator.rzk
376396
# ^ source.rzk
377397
# ^ source.rzk keyword.operator.rzk
378398
# ^ source.rzk
379-
# ^^ source.rzk punctuation.definition.modtype.rzk
399+
# ^ source.rzk keyword.operator.rzk
400+
# ^ source.rzk keyword.operator.rzk
380401
# ^ source.rzk
381402
# ^ source.rzk entity.name.tag.rzk
382403
# ^ source.rzk
383404
# ^ source.rzk keyword.operator.rzk
384405
# ^^^ source.rzk
385-
# ^^ source.rzk punctuation.definition.modtype.rzk
406+
# ^ source.rzk keyword.operator.rzk
407+
# ^ source.rzk keyword.operator.rzk
386408
> :=
387409
#^^ source.rzk
388410
# ^^ source.rzk keyword.operator.rzk
@@ -424,33 +446,39 @@
424446
# ^ source.rzk
425447
# ^ source.rzk keyword.operator.colon.params.rzk
426448
# ^ source.rzk
427-
# ^^ source.rzk punctuation.definition.modtype.rzk
449+
# ^ source.rzk keyword.operator.rzk
450+
# ^ source.rzk keyword.operator.rzk
428451
# ^ source.rzk
429452
# ^ source.rzk entity.name.tag.rzk
430453
# ^ source.rzk
431454
# ^ source.rzk keyword.operator.rzk
432455
# ^ source.rzk
433-
# ^^ source.rzk punctuation.definition.modtype.rzk
456+
# ^ source.rzk keyword.operator.rzk
457+
# ^ source.rzk keyword.operator.rzk
434458
# ^ source.rzk
435459
# ^ source.rzk entity.name.tag.rzk
436460
# ^ source.rzk
437461
# ^ source.rzk keyword.operator.rzk
438462
# ^^^ source.rzk
439-
# ^^ source.rzk punctuation.definition.modtype.rzk
463+
# ^ source.rzk keyword.operator.rzk
464+
# ^ source.rzk keyword.operator.rzk
440465
# ^ source.rzk
441-
# ^^ source.rzk punctuation.definition.modtype.rzk
466+
# ^ source.rzk keyword.operator.rzk
467+
# ^ source.rzk keyword.operator.rzk
442468
# ^ source.rzk
443469
> : <| ♯ | A |>
444470
#^^ source.rzk
445471
# ^ source.rzk keyword.operator.rzk
446472
# ^ source.rzk
447-
# ^^ source.rzk punctuation.definition.modtype.rzk
473+
# ^ source.rzk keyword.operator.rzk
474+
# ^ source.rzk keyword.operator.rzk
448475
# ^ source.rzk
449476
# ^ source.rzk entity.name.tag.rzk
450477
# ^ source.rzk
451478
# ^ source.rzk keyword.operator.rzk
452479
# ^^^ source.rzk
453-
# ^^ source.rzk punctuation.definition.modtype.rzk
480+
# ^ source.rzk keyword.operator.rzk
481+
# ^ source.rzk keyword.operator.rzk
454482
> :=
455483
#^^ source.rzk
456484
# ^^ source.rzk keyword.operator.rzk
@@ -489,15 +517,17 @@
489517
#^^ source.rzk
490518
# ^ source.rzk keyword.operator.rzk
491519
# ^ source.rzk
492-
# ^^ source.rzk punctuation.definition.modtype.rzk
520+
# ^ source.rzk keyword.operator.rzk
521+
# ^ source.rzk keyword.operator.rzk
493522
# ^ source.rzk
494523
# ^ source.rzk entity.name.tag.rzk
495524
# ^ source.rzk
496525
# ^ source.rzk keyword.operator.rzk
497526
# ^ source.rzk
498527
# ^ source.rzk support.type.rzk
499528
# ^ source.rzk
500-
# ^^ source.rzk punctuation.definition.modtype.rzk
529+
# ^ source.rzk keyword.operator.rzk
530+
# ^ source.rzk keyword.operator.rzk
501531
> := mod ♭ U
502532
#^^ source.rzk
503533
# ^^ source.rzk keyword.operator.rzk
@@ -542,15 +572,17 @@
542572
#^^ source.rzk
543573
# ^ source.rzk keyword.operator.rzk
544574
# ^ source.rzk
545-
# ^^ source.rzk punctuation.definition.modtype.rzk
575+
# ^ source.rzk keyword.operator.rzk
576+
# ^ source.rzk keyword.operator.rzk
546577
# ^ source.rzk
547578
# ^ source.rzk entity.name.tag.rzk
548579
# ^ source.rzk
549580
# ^ source.rzk keyword.operator.rzk
550581
# ^ source.rzk
551582
# ^ source.rzk support.type.rzk
552583
# ^ source.rzk
553-
# ^^ source.rzk punctuation.definition.modtype.rzk
584+
# ^ source.rzk keyword.operator.rzk
585+
# ^ source.rzk keyword.operator.rzk
554586
> := mod ♭ prop
555587
#^^ source.rzk
556588
# ^^ source.rzk keyword.operator.rzk
@@ -595,15 +627,17 @@
595627
#^^ source.rzk
596628
# ^ source.rzk keyword.operator.rzk
597629
# ^ source.rzk
598-
# ^^ source.rzk punctuation.definition.modtype.rzk
630+
# ^ source.rzk keyword.operator.rzk
631+
# ^ source.rzk keyword.operator.rzk
599632
# ^ source.rzk
600633
# ^ source.rzk entity.name.tag.rzk
601634
# ^ source.rzk
602635
# ^ source.rzk keyword.operator.rzk
603636
# ^ source.rzk
604637
# ^ source.rzk support.type.rzk
605638
# ^ source.rzk
606-
# ^^ source.rzk punctuation.definition.modtype.rzk
639+
# ^ source.rzk keyword.operator.rzk
640+
# ^ source.rzk keyword.operator.rzk
607641
> := mod ♭ univ-family-prop
608642
#^^ source.rzk
609643
# ^^ source.rzk keyword.operator.rzk
@@ -621,15 +655,17 @@
621655
#^^ source.rzk
622656
# ^ source.rzk keyword.operator.rzk
623657
# ^ source.rzk
624-
# ^^ source.rzk punctuation.definition.modtype.rzk
658+
# ^ source.rzk keyword.operator.rzk
659+
# ^ source.rzk keyword.operator.rzk
625660
# ^ source.rzk
626661
# ^ source.rzk entity.name.tag.rzk
627662
# ^ source.rzk
628663
# ^ source.rzk keyword.operator.rzk
629664
# ^ source.rzk
630665
# ^ source.rzk support.type.rzk
631666
# ^ source.rzk
632-
# ^^ source.rzk punctuation.definition.modtype.rzk
667+
# ^ source.rzk keyword.operator.rzk
668+
# ^ source.rzk keyword.operator.rzk
633669
> := mod ♭ Unit
634670
#^^ source.rzk
635671
# ^^ source.rzk keyword.operator.rzk
@@ -662,13 +698,15 @@
662698
# ^ source.rzk
663699
# ^ source.rzk keyword.operator.colon.params.rzk
664700
# ^ source.rzk
665-
# ^^ source.rzk punctuation.definition.modtype.rzk
701+
# ^ source.rzk keyword.operator.rzk
702+
# ^ source.rzk keyword.operator.rzk
666703
# ^ source.rzk
667704
# ^ source.rzk entity.name.tag.rzk
668705
# ^ source.rzk
669706
# ^ source.rzk keyword.operator.rzk
670707
# ^^^ source.rzk
671-
# ^^ source.rzk punctuation.definition.modtype.rzk
708+
# ^ source.rzk keyword.operator.rzk
709+
# ^ source.rzk keyword.operator.rzk
672710
# ^ source.rzk
673711
> ( p : x = y)
674712
#^^ source.rzk
@@ -698,13 +736,15 @@
698736
#^^ source.rzk
699737
# ^^ source.rzk keyword.operator.rzk
700738
# ^^^^ source.rzk
701-
# ^^ source.rzk punctuation.definition.modtype.rzk
739+
# ^ source.rzk keyword.operator.rzk
740+
# ^ source.rzk keyword.operator.rzk
702741
# ^ source.rzk
703742
# ^ source.rzk entity.name.tag.rzk
704743
# ^ source.rzk
705744
# ^ source.rzk keyword.operator.rzk
706745
# ^^^ source.rzk
707-
# ^^ source.rzk punctuation.definition.modtype.rzk
746+
# ^ source.rzk keyword.operator.rzk
747+
# ^ source.rzk keyword.operator.rzk
708748
# ^^^^^^^^^^^^^^^^^^^ source.rzk
709749
# ^^^ source.rzk support.function.rzk
710750
# ^ source.rzk

0 commit comments

Comments
 (0)