diff options
author | Tim Baumann <tim@timbaumann.info> | 2013-05-19 02:31:57 +0200 |
---|---|---|
committer | Tim Baumann <tim@timbaumann.info> | 2013-05-19 02:31:57 +0200 |
commit | f91963a6ffd4d17e338e1d4ee3b9171889fc45b0 (patch) | |
tree | ef0acc704c847071bd11147f276a1f6045c0407b | |
parent | c3be8e9b4f0396cf68ca5f02e5f72ee6d4c90003 (diff) | |
download | pygments-f91963a6ffd4d17e338e1d4ee3b9171889fc45b0.tar.gz |
Added lexer for Agda
-rw-r--r-- | pygments/lexers/_mapping.py | 1 | ||||
-rw-r--r-- | pygments/lexers/functional.py | 74 |
2 files changed, 73 insertions, 2 deletions
diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py index bcb17e5a..b29d8262 100644 --- a/pygments/lexers/_mapping.py +++ b/pygments/lexers/_mapping.py @@ -18,6 +18,7 @@ LEXERS = { 'ActionScript3Lexer': ('pygments.lexers.web', 'ActionScript 3', ('as3', 'actionscript3'), ('*.as',), ('application/x-actionscript', 'text/x-actionscript', 'text/actionscript')), 'ActionScriptLexer': ('pygments.lexers.web', 'ActionScript', ('as', 'actionscript'), ('*.as',), ('application/x-actionscript3', 'text/x-actionscript3', 'text/actionscript3')), 'AdaLexer': ('pygments.lexers.compiled', 'Ada', ('ada', 'ada95ada2005'), ('*.adb', '*.ads', '*.ada'), ('text/x-ada',)), + 'AgdaLexer': ('pygments.lexers.functional', 'Agda', ('agda',), ('*.agda',), ('text/x-agda',)), 'AntlrActionScriptLexer': ('pygments.lexers.parsers', 'ANTLR With ActionScript Target', ('antlr-as', 'antlr-actionscript'), ('*.G', '*.g'), ()), 'AntlrCSharpLexer': ('pygments.lexers.parsers', 'ANTLR With C# Target', ('antlr-csharp', 'antlr-c#'), ('*.G', '*.g'), ()), 'AntlrCppLexer': ('pygments.lexers.parsers', 'ANTLR With CPP Target', ('antlr-cpp',), ('*.G', '*.g'), ()), diff --git a/pygments/lexers/functional.py b/pygments/lexers/functional.py index 613be987..32e557ca 100644 --- a/pygments/lexers/functional.py +++ b/pygments/lexers/functional.py @@ -17,8 +17,8 @@ from pygments.token import Text, Comment, Operator, Keyword, Name, \ __all__ = ['RacketLexer', 'SchemeLexer', 'CommonLispLexer', 'HaskellLexer', 'LiterateHaskellLexer', 'SMLLexer', 'OcamlLexer', 'ErlangLexer', - 'ErlangShellLexer', 'OpaLexer', 'CoqLexer', 'NewLispLexer', - 'ElixirLexer', 'ElixirConsoleLexer', 'KokaLexer'] + 'ErlangShellLexer', 'OpaLexer', 'CoqLexer', 'AgdaLexer', + 'NewLispLexer', 'ElixirLexer', 'ElixirConsoleLexer', 'KokaLexer'] class RacketLexer(RegexLexer): @@ -1081,6 +1081,76 @@ class LiterateHaskellLexer(Lexer): yield item +class AgdaLexer(RegexLexer): + """ + For the `Agda <http://wiki.portal.chalmers.se/agda/pmwiki.php>`_ + dependently typed functional programming language and proof assistant. + """ + + name = 'Agda' + aliases = ['agda'] + filenames = ['*.agda'] + mimetypes = ['text/x-agda'] + + reserved = ['abstract', 'codata', 'coinductive', 'data', 'field', + 'forall', 'hiding', 'in', 'inductive', 'infix', 'infixl', + 'infixr', 'let', 'open', 'pattern', 'primitive', 'private', + 'mutual', 'quote', 'quoteGoal', 'quoteTerm', 'record', + 'syntax', 'rewrite', 'unquote', 'using', 'where', 'with'] + + tokens = { + 'root': [ + # Declaration + (r'^(\s*)([^\s\(\)\{\}]+)(\s*)(:)(\s*)', bygroups(Text, Name.Function, Text, Operator.Word, Text)), + (r'\s+', Text), # Whitespace + # Comments + (r'--(?![!#$%&*+./<=>?@\^|_~:\\]).*?$', Comment.Single), + (r'{-', Comment.Multiline, 'comment'), + # Holes + (r'{!', Comment.Directive, 'hole'), + # Lexemes: + # Identifiers + (ur'\b(%s)(?!\')\b' % '|'.join(reserved), Keyword.Reserved), + (r'(import)(\s+)([A-Z][a-zA-Z0-9_.]*)', bygroups(Keyword.Reserved, Text, Name)), + (r'(module)(\s+)([A-Z][a-zA-Z0-9_.]*)', bygroups(Keyword.Reserved, Text, Name)), + (r'\b(Set|Prop)\b', Keyword.Type), + # Special Symbols + (r'(\(|\)|\{|\})', Operator), + (ur'(\.{1,3}|\||[\u039B]|[\u2200]|[\u2192]|:|=|->)', Operator.Word), + #(r'\\(?![:!#$%&*+.\\/<=>?@^|~-]+)', Name.Function), # lambda operator + #(r'(<-|::|->|=>|=)(?![:!#$%&*+.\\/<=>?@^|~-]+)', Operator.Word), # specials + #(r':[:!#$%&*+.\\/<=>?@^|~-]*', Keyword.Type), # Constructor operators + #(r'[:!#$%&*+.\\/<=>?@^|~-]+', Operator), # Other operators + # Numbers + (r'\d+[eE][+-]?\d+', Number.Float), + (r'\d+\.\d+([eE][+-]?\d+)?', Number.Float), + (r'0[xX][\da-fA-F]+', Number.Hex), + (r'\d+', Number.Integer), + # Strings + (r"'", String.Char, 'character'), + (r'"', String, 'string'), + (r'[^\s\(\)\{\}]+', Text), + ], + 'comment': [ + # Multiline Comments + (r'[^-{}]+', Comment.Multiline), + (r'{-', Comment.Multiline, '#push'), + (r'-}', Comment.Multiline, '#pop'), + (r'[-{}]', Comment.Multiline), + ], + 'hole': [ + # Holes + (r'[^!{}]+', Comment.Directive), + (r'{!', Comment.Directive, '#push'), + (r'!}', Comment.Directive, '#pop'), + (r'[!{}]', Comment.Directive), + ], + 'character': HaskellLexer.tokens['character'], + 'string': HaskellLexer.tokens['string'], + 'escape': HaskellLexer.tokens['escape'] + } + + class SMLLexer(RegexLexer): """ For the Standard ML language. |