Merge pull request #1 from rzk-lang/unicode-syntax

Support unicode syntax and fix some token types

pygments_rzk/__init__.py

@@ -35,34 +35,34 @@ def get_tokens_unprocessed(self, text):
             (r'^(#check|#compute(-whnf|-nf)?|#set-option|#unset-option)(?=$|[.\\;,#"\]\[)(}{><|\s-])',
              bygroups(Name.Decorator)),
             (r'^(#section|#end)(\s+(?![-?!.])[^.\\;,#"\]\[)(}{><|\s]*)?(?=$|[.\\;,#"\]\[)(}{><|\s])',
-             bygroups(Name.Decorator, Name.Entity)),
+             bygroups(Name.Decorator, Name)),
             (r'^(#assume|#variable|#variables)(\s+)((?![-?!.])[^.\\;,#"\]\[)(}{><|:]*)(?=$|[.\\;,#"\]\[)(}{><|\s])',
-             bygroups(Keyword.Declaration, Punctuation, Name.Variable)),
+             bygroups(Keyword.Reserved, Punctuation, Text)),
             (r'^(#def|#define|#postulate)(\s+)((?![-?!.])[^.\\;,#"\]\[)(}{><|\s]*)(?=$|[.\\;,#"\]\[)(}{><|\s])((\s+)(uses)(\s+\()((?![-?!.])[^.\\;,#"\]\[)(}{><|]*)(\)))?',
-             bygroups(Keyword.Declaration, Punctuation, Name.Function, None, Punctuation, Keyword, Punctuation, Name.Variable, Punctuation)),
+             bygroups(Keyword.Reserved, Punctuation, Name.Function, None, Punctuation, Keyword, Punctuation, Text, Punctuation)),
 
             # bultins
-            (r'(?<=[.\\;,#"\]\[)(}{><|\s])(CUBE|TOPE|U(nit)?|𝒰)(?=$|[.\\;,#"\]\[)(}{><|\s])',
+            (r'(?<=[.\\;,#"\]\[)(}{><|\s])(CUBE|TOPE|U(nit)?)(?=$|[.\\;,#"\]\[)(}{><|\s])',
              Keyword.Type),
-            (r'(?<=[.\\;,#"\]\[)(}{><|\s])(1|2|𝟙|𝟚|Sigma|∑|Σ)(?=$|[.\\;,#"\]\[)(}{><|\s])',
+            (r'(?<=[.\\;,#"\]\[)(}{><|\s])(1|2|Sigma|∑|Σ)(?=$|[.\\;,#"\]\[)(}{><|\s])',
              Keyword.Type),
-            (r'(===|<=|\\/|/\\)',
-             Operator),
-            (r'(⊤|⊥|\*_1|⋆)|(?<=[.\\;,#"\]\[)(}{><|\s])(0_2|1_2|TOP|BOT)(?=$|[.\\;,#"\]\[)(}{><|\s])',
-             Name.Constant),
-            (r'(?<=[.\\;,#"\]\[)(}{><|\s])(recOR|rec∨|recBOT|rec⊥|idJ|refl|first|second|π₁|π₂|unit)((?=$|[.\\;,#"\]\[)(}{><|\s])|(?=_{))',
-             Name.Constant),
+            (r'(===|≡|<=|≤|\\/|∨|/\\|∧)',
+             String.Other),
+            (r'(⊤|⊥|\*_1|\*₁)|(?<=[.\\;,#"\]\[)(}{><|\s])(0_2|0₂|1_2|1₂|TOP|BOT)(?=$|[.\\;,#"\]\[)(}{><|\s])',
+             Number),
+            (r'(?<=[.\\;,#"\]\[)(}{><|\s])(recOR|recBOT|idJ|refl|first|second|π₁|π₂|unit)((?=$|[.\\;,#"\]\[)(}{><|\s])|(?=_{))',
+             String),
             (r'(?<=[.\\;,#"\]\[)(}{><|\s])as(?=$|[.\\;,#"\]\[)(}{><|\s])',
-             Keyword),
+             Keyword.Reserved),
 
             # parameters
             (r'(\(\s*)([^{:\)]+\s*)(:)(?=$|[.\\;,#"\]\[)(}{><|\s])',
-             bygroups(Punctuation, Name.Variable, Punctuation)),
+             bygroups(Punctuation, Text, Punctuation)),
 
             (r'"', String, 'string'),
 
-            (r'(\\\s*)((([^\t\n\r !"#\(\),-\.;:\\\/=<>\?\[\\\]\{\|\}][^\t\n\r !"#\(\),\.;:<>\?\[\\\]\{\|\}]*)\s*)+)',
-                bygroups(Punctuation, Name.Variable)),
+            (r'(\\\s*)((([^→\t\n\r !"#\(\),-\.;:\\\/=<>\?\[\\\]\{\|\}][^\t\n\r !"#\(\),\.;:<>\?\[\\\]\{\|\}]*)\s*)+)',
+                bygroups(Punctuation, Text)),
         ],
         'string': [
             (r'[^"]+', String),