mirror of
https://github.com/alecthomas/chroma.git
synced 2025-03-17 20:58:08 +02:00
Add an Agda lexer (#891)
This commit is contained in:
parent
d9f6ed634e
commit
08be6f023f
@ -38,7 +38,7 @@ translators for Pygments lexers and styles.
|
||||
|
||||
| Prefix | Language |
|
||||
| :----: | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
|
||||
| A | ABAP, ABNF, ActionScript, ActionScript 3, Ada, AL, Angular2, ANTLR, ApacheConf, APL, AppleScript, ArangoDB AQL, Arduino, ArmAsm, AutoHotkey, AutoIt, Awk |
|
||||
| A | ABAP, ABNF, ActionScript, ActionScript 3, Ada, Agda, AL, Angular2, ANTLR, ApacheConf, APL, AppleScript, ArangoDB AQL, Arduino, ArmAsm, AutoHotkey, AutoIt, Awk |
|
||||
| B | Ballerina, Bash, Bash Session, Batchfile, BibTeX, Bicep, BlitzBasic, BNF, BQN, Brainfuck |
|
||||
| C | C, C#, C++, Caddyfile, Caddyfile Directives, Cap'n Proto, Cassandra CQL, Ceylon, CFEngine3, cfstatement, ChaiScript, Chapel, Cheetah, Clojure, CMake, COBOL, CoffeeScript, Common Lisp, Coq, Crystal, CSS, Cython |
|
||||
| D | D, Dart, Dax, Diff, Django/Jinja, dns, Docker, DTD, Dylan |
|
||||
|
66
lexers/embedded/agda.xml
Normal file
66
lexers/embedded/agda.xml
Normal file
@ -0,0 +1,66 @@
|
||||
<lexer>
|
||||
<config>
|
||||
<name>Agda</name>
|
||||
<alias>agda</alias>
|
||||
<filename>*.agda</filename>
|
||||
<mime_type>text/x-agda</mime_type>
|
||||
</config>
|
||||
<rules>
|
||||
<state name="root">
|
||||
<rule pattern="^(\s*)([^\s(){}]+)(\s*)(:)(\s*)"><bygroups><token type="TextWhitespace"/><token type="NameFunction"/><token type="TextWhitespace"/><token type="OperatorWord"/><token type="TextWhitespace"/></bygroups></rule>
|
||||
<rule pattern="--(?![!#$%&*+./<=>?@^|_~:\\]).*?$"><token type="CommentSingle"/></rule>
|
||||
<rule pattern="\{-"><token type="CommentMultiline"/><push state="comment"/></rule>
|
||||
<rule pattern="\{!"><token type="CommentMultiline"/><push state="hole"/></rule>
|
||||
<rule pattern="\b(abstract|codata|coinductive|constructor|data|do|eta-equality|field|forall|hiding|in|inductive|infix|infixl|infixr|instance|interleaved|let|macro|mutual|no-eta-equality|open|overlap|pattern|postulate|primitive|private|quote|quoteTerm|record|renaming|rewrite|syntax|tactic|unquote|unquoteDecl|unquoteDef|using|variable|where|with)(?!\')\b"><token type="KeywordReserved"/></rule>
|
||||
<rule pattern="(import|module)(\s+)"><bygroups><token type="KeywordReserved"/><token type="TextWhitespace"/></bygroups><push state="module"/></rule>
|
||||
<rule pattern="\b(Set|Prop)[\u2080-\u2089]*\b"><token type="KeywordType"/></rule>
|
||||
<rule pattern="(\(|\)|\{|\})"><token type="Operator"/></rule>
|
||||
<rule pattern="(\.{1,3}|\||\u03BB|\u2200|\u2192|:|=|->)"><token type="OperatorWord"/></rule>
|
||||
<rule pattern="\d+[eE][+-]?\d+"><token type="LiteralNumberFloat"/></rule>
|
||||
<rule pattern="\d+\.\d+([eE][+-]?\d+)?"><token type="LiteralNumberFloat"/></rule>
|
||||
<rule pattern="0[xX][\da-fA-F]+"><token type="LiteralNumberHex"/></rule>
|
||||
<rule pattern="\d+"><token type="LiteralNumberInteger"/></rule>
|
||||
<rule pattern="'"><token type="LiteralStringChar"/><push state="character"/></rule>
|
||||
<rule pattern="""><token type="LiteralString"/><push state="string"/></rule>
|
||||
<rule pattern="[^\s(){}]+"><token type="Text"/></rule>
|
||||
<rule pattern="\s+?"><token type="TextWhitespace"/></rule>
|
||||
</state>
|
||||
<state name="hole">
|
||||
<rule pattern="[^!{}]+"><token type="CommentMultiline"/></rule>
|
||||
<rule pattern="\{!"><token type="CommentMultiline"/><push/></rule>
|
||||
<rule pattern="!\}"><token type="CommentMultiline"/><pop depth="1"/></rule>
|
||||
<rule pattern="[!{}]"><token type="CommentMultiline"/></rule>
|
||||
</state>
|
||||
<state name="module">
|
||||
<rule pattern="\{-"><token type="CommentMultiline"/><push state="comment"/></rule>
|
||||
<rule pattern="[a-zA-Z][\w.\']*"><token type="Name"/><pop depth="1"/></rule>
|
||||
<rule pattern="[\W0-9_]+"><token type="Text"/></rule>
|
||||
</state>
|
||||
<state name="comment">
|
||||
<rule pattern="[^-{}]+"><token type="CommentMultiline"/></rule>
|
||||
<rule pattern="\{-"><token type="CommentMultiline"/><push/></rule>
|
||||
<rule pattern="-\}"><token type="CommentMultiline"/><pop depth="1"/></rule>
|
||||
<rule pattern="[-{}]"><token type="CommentMultiline"/></rule>
|
||||
</state>
|
||||
<state name="character">
|
||||
<rule pattern="[^\\']'"><token type="LiteralStringChar"/><pop depth="1"/></rule>
|
||||
<rule pattern="\\"><token type="LiteralStringEscape"/><push state="escape"/></rule>
|
||||
<rule pattern="'"><token type="LiteralStringChar"/><pop depth="1"/></rule>
|
||||
</state>
|
||||
<state name="string">
|
||||
<rule pattern="[^\\"]+"><token type="LiteralString"/></rule>
|
||||
<rule pattern="\\"><token type="LiteralStringEscape"/><push state="escape"/></rule>
|
||||
<rule pattern="""><token type="LiteralString"/><pop depth="1"/></rule>
|
||||
</state>
|
||||
<state name="escape">
|
||||
<rule pattern="[abfnrtv"\'&\\]"><token type="LiteralStringEscape"/><pop depth="1"/></rule>
|
||||
<rule pattern="\^[][A-ZÀ-ÖØ-ÞĀĂĄĆĈĊČĎĐĒĔĖĘĚĜĞĠĢĤĦĨĪĬĮİIJĴĶĹĻĽĿŁŃŅŇŊŌŎŐŒŔŖŘŚŜŞŠŢŤŦŨŪŬŮŰŲŴŶŸ-ŹŻŽƁ-ƂƄƆ-ƇƉ-ƋƎ-ƑƓ-ƔƖ-ƘƜ-ƝƟ-ƠƢƤƦ-ƧƩƬƮ-ƯƱ-ƳƵƷ-ƸƼDŽLJNJǍǏǑǓǕǗǙǛǞǠǢǤǦǨǪǬǮDZǴǶ-ǸǺǼǾȀȂȄȆȈȊȌȎȐȒȔȖȘȚȜȞȠȢȤȦȨȪȬȮȰȲȺ-ȻȽ-ȾɁɃ-ɆɈɊɌɎͰͲͶͿΆΈ-ΊΌΎ-ΏΑ-ΡΣ-ΫϏϒ-ϔϘϚϜϞϠϢϤϦϨϪϬϮϴϷϹ-ϺϽ-ЯѠѢѤѦѨѪѬѮѰѲѴѶѸѺѼѾҀҊҌҎҐҒҔҖҘҚҜҞҠҢҤҦҨҪҬҮҰҲҴҶҸҺҼҾӀ-ӁӃӅӇӉӋӍӐӒӔӖӘӚӜӞӠӢӤӦӨӪӬӮӰӲӴӶӸӺӼӾԀԂԄԆԈԊԌԎԐԒԔԖԘԚԜԞԠԢԤԦԨԪԬԮԱ-ՖႠ-ჅჇჍᎠ-ᏵᲐ-ᲺᲽ-ᲿḀḂḄḆḈḊḌḎḐḒḔḖḘḚḜḞḠḢḤḦḨḪḬḮḰḲḴḶḸḺḼḾṀṂṄṆṈṊṌṎṐṒṔṖṘṚṜṞṠṢṤṦṨṪṬṮṰṲṴṶṸṺṼṾẀẂẄẆẈẊẌẎẐẒẔẞẠẢẤẦẨẪẬẮẰẲẴẶẸẺẼẾỀỂỄỆỈỊỌỎỐỒỔỖỘỚỜỞỠỢỤỦỨỪỬỮỰỲỴỶỸỺỼỾἈ-ἏἘ-ἝἨ-ἯἸ-ἿὈ-ὍὙὛὝὟὨ-ὯᾸ-ΆῈ-ΉῘ-ΊῨ-ῬῸ-Ώℂℇℋ-ℍℐ-ℒℕℙ-ℝℤΩℨK-ℭℰ-ℳℾ-ℿⅅↃⰀ-ⰮⱠⱢ-ⱤⱧⱩⱫⱭ-ⱰⱲⱵⱾ-ⲀⲂⲄⲆⲈⲊⲌⲎⲐⲒⲔⲖⲘⲚⲜⲞⲠⲢⲤⲦⲨⲪⲬⲮⲰⲲⲴⲶⲸⲺⲼⲾⳀⳂⳄⳆⳈⳊⳌⳎⳐⳒⳔⳖⳘⳚⳜⳞⳠⳢⳫⳭⳲꙀꙂꙄꙆꙈꙊꙌꙎꙐꙒꙔꙖꙘꙚꙜꙞꙠꙢꙤꙦꙨꙪꙬꚀꚂꚄꚆꚈꚊꚌꚎꚐꚒꚔꚖꚘꚚꜢꜤꜦꜨꜪꜬꜮꜲꜴꜶꜸꜺꜼꜾꝀꝂꝄꝆꝈꝊꝌꝎꝐꝒꝔꝖꝘꝚꝜꝞꝠꝢꝤꝦꝨꝪꝬꝮꝹꝻꝽ-ꝾꞀꞂꞄꞆꞋꞍꞐꞒꞖꞘꞚꞜꞞꞠꞢꞤꞦꞨꞪ-ꞮꞰ-ꞴꞶꞸA-Z𐐀-𐐧𐒰-𐓓𐲀-𐲲𑢠-𑢿𖹀-𖹟𝐀-𝐙𝐴-𝑍𝑨-𝒁𝒜𝒞-𝒟𝒢𝒥-𝒦𝒩-𝒬𝒮-𝒵𝓐-𝓩𝔄-𝔅𝔇-𝔊𝔍-𝔔𝔖-𝔜𝔸-𝔹𝔻-𝔾𝕀-𝕄𝕆𝕊-𝕐𝕬-𝖅𝖠-𝖹𝗔-𝗭𝘈-𝘡𝘼-𝙕𝙰-𝚉𝚨-𝛀𝛢-𝛺𝜜-𝜴𝝖-𝝮𝞐-𝞨𝟊𞤀-𞤡@^_]"><token type="LiteralStringEscape"/><pop depth="1"/></rule>
|
||||
<rule pattern="NUL|SOH|[SE]TX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|S[OI]|DLE|DC[1-4]|NAK|SYN|ETB|CAN|EM|SUB|ESC|[FGRU]S|SP|DEL"><token type="LiteralStringEscape"/><pop depth="1"/></rule>
|
||||
<rule pattern="o[0-7]+"><token type="LiteralStringEscape"/><pop depth="1"/></rule>
|
||||
<rule pattern="x[\da-fA-F]+"><token type="LiteralStringEscape"/><pop depth="1"/></rule>
|
||||
<rule pattern="\d+"><token type="LiteralStringEscape"/><pop depth="1"/></rule>
|
||||
<rule pattern="(\s+)(\\)"><bygroups><token type="TextWhitespace"/><token type="LiteralStringEscape"/></bygroups><pop depth="1"/></rule>
|
||||
</state>
|
||||
</rules>
|
||||
</lexer>
|
||||
|
12
lexers/testdata/agda.actual
vendored
Normal file
12
lexers/testdata/agda.actual
vendored
Normal file
@ -0,0 +1,12 @@
|
||||
module hello-world where
|
||||
|
||||
open import Agda.Builtin.IO using (IO)
|
||||
open import Agda.Builtin.Unit using (⊤)
|
||||
open import Agda.Builtin.String using (String)
|
||||
|
||||
postulate putStrLn : String → IO ⊤
|
||||
{-# FOREIGN GHC import qualified Data.Text as T #-}
|
||||
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
|
||||
|
||||
main : IO ⊤
|
||||
main = putStrLn "Hello world!"
|
79
lexers/testdata/agda.expected
vendored
Normal file
79
lexers/testdata/agda.expected
vendored
Normal file
@ -0,0 +1,79 @@
|
||||
[
|
||||
{"type":"KeywordReserved","value":"module"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Name","value":"hello"},
|
||||
{"type":"Text","value":"-world"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"where"},
|
||||
{"type":"TextWhitespace","value":"\n\n"},
|
||||
{"type":"KeywordReserved","value":"open"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"import"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Name","value":"Agda.Builtin.IO"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"using"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Operator","value":"("},
|
||||
{"type":"Text","value":"IO"},
|
||||
{"type":"Operator","value":")"},
|
||||
{"type":"TextWhitespace","value":"\n"},
|
||||
{"type":"KeywordReserved","value":"open"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"import"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Name","value":"Agda.Builtin.Unit"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"using"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Operator","value":"("},
|
||||
{"type":"Text","value":"⊤"},
|
||||
{"type":"Operator","value":")"},
|
||||
{"type":"TextWhitespace","value":"\n"},
|
||||
{"type":"KeywordReserved","value":"open"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"import"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Name","value":"Agda.Builtin.String"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"KeywordReserved","value":"using"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Operator","value":"("},
|
||||
{"type":"Text","value":"String"},
|
||||
{"type":"Operator","value":")"},
|
||||
{"type":"TextWhitespace","value":"\n\n"},
|
||||
{"type":"KeywordReserved","value":"postulate"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"putStrLn"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"OperatorWord","value":":"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"String"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"OperatorWord","value":"→"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"IO"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"⊤"},
|
||||
{"type":"TextWhitespace","value":"\n"},
|
||||
{"type":"CommentMultiline","value":"{-# FOREIGN GHC import qualified Data.Text as T #-}"},
|
||||
{"type":"TextWhitespace","value":"\n"},
|
||||
{"type":"CommentMultiline","value":"{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}"},
|
||||
{"type":"TextWhitespace","value":"\n\n"},
|
||||
{"type":"NameFunction","value":"main"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"OperatorWord","value":":"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"IO"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"⊤"},
|
||||
{"type":"TextWhitespace","value":"\n"},
|
||||
{"type":"Text","value":"main"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"OperatorWord","value":"="},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"Text","value":"putStrLn"},
|
||||
{"type":"TextWhitespace","value":" "},
|
||||
{"type":"LiteralString","value":"\"Hello world!\""},
|
||||
{"type":"TextWhitespace","value":"\n"}
|
||||
]
|
Loading…
x
Reference in New Issue
Block a user