Commits

Haohui Mai committed e883809

Implement the lexer of the Dafny language.

  • Participants
  • Parent commits 8731624

Comments (0)

Files changed (2)

File pygments/lexers/_mapping.py

     'CssSmartyLexer': ('pygments.lexers.templates', 'CSS+Smarty', ('css+smarty',), (), ('text/css+smarty',)),
     'CudaLexer': ('pygments.lexers.compiled', 'CUDA', ('cuda', 'cu'), ('*.cu', '*.cuh'), ('text/x-cuda',)),
     'CythonLexer': ('pygments.lexers.compiled', 'Cython', ('cython', 'pyx'), ('*.pyx', '*.pxd', '*.pxi'), ('text/x-cython', 'application/x-cython')),
+    'DafnyLexer': ('pygments.lexers.dafny', 'Dafny', ('dafny',), ('*.dfy',), ('text/x-dafny',)),
     'DLexer': ('pygments.lexers.compiled', 'D', ('d',), ('*.d', '*.di'), ('text/x-dsrc',)),
     'DObjdumpLexer': ('pygments.lexers.asm', 'd-objdump', ('d-objdump',), ('*.d-objdump',), ('text/x-d-objdump',)),
     'DarcsPatchLexer': ('pygments.lexers.text', 'Darcs Patch', ('dpatch',), ('*.dpatch', '*.darcspatch'), ()),

File pygments/lexers/dafny.py

+# -*- coding: utf-8 -*-
+"""
+    pygments.lexers.dafny
+    ~~~~~~~~~~~~~~~~~~~~~
+
+    Pygments lexers for the Dafny language.
+
+    :copyright: Copyright 2006-2013 by the Pygments team, see AUTHORS.
+    :license: BSD, see LICENSE for details.
+"""
+import re
+
+from pygments.lexer import RegexLexer, DelegatingLexer, bygroups, include, \
+     using, this
+from pygments.token import Punctuation, \
+     Text, Comment, Operator, Keyword, Name, String, Number, Literal, Other
+
+from pygments.token import *
+
+from pygments.util import get_choice_opt
+from pygments import unistring as uni
+
+__all__ = ['DafnyLexer']
+
+class DafnyLexer(RegexLexer):
+    """
+    For `Dafny <http://research.microsoft.com/en-us/projects/dafny>`_
+    source code.
+
+    Additional options accepted:
+
+    `unicodelevel`
+      Determines which Unicode characters this lexer allows for identifiers.
+      The possible values are:
+
+      * ``none`` -- only the ASCII letters and numbers are allowed. This
+        is the fastest selection.
+      * ``basic`` -- all Unicode characters from the specification except
+        category ``Lo`` are allowed.
+      * ``full`` -- all Unicode characters as specified in the C# specs
+        are allowed.  Note that this means a considerable slowdown since the
+        ``Lo`` category has more than 40,000 characters in it!
+
+      The default value is ``basic``.
+
+      *New in Pygments 0.8.*
+    """
+
+    name = 'Dafny'
+    aliases = ['dafny']
+    filenames = ['*.dfy']
+    mimetypes = ['text/x-dafny']
+
+    flags = re.MULTILINE | re.DOTALL | re.UNICODE
+
+    # for the range of allowed unicode characters in identifiers, see
+    # http://www.ecma-international.org/publications/files/ECMA-ST/Ecma-334.pdf
+
+    levels = dict(
+        none = '@?[_a-zA-Z][a-zA-Z0-9_]*',
+        basic = ('@?[_' + uni.Lu + uni.Ll + uni.Lt + uni.Lm + uni.Nl + ']' +
+                 '[' + uni.Lu + uni.Ll + uni.Lt + uni.Lm + uni.Nl +
+                 uni.Nd + uni.Pc + uni.Cf + uni.Mn + uni.Mc + ']*'),
+        full = ('@?(?:_|[^' + uni.allexcept('Lu', 'Ll', 'Lt', 'Lm', 'Lo',
+                                            'Nl') + '])'
+                + '[^' + uni.allexcept('Lu', 'Ll', 'Lt', 'Lm', 'Lo', 'Nl',
+                                       'Nd', 'Pc', 'Cf', 'Mn', 'Mc') + ']*'),
+    )
+
+    tokens = {}
+    token_variants = True
+
+    for levelname, cs_ident in levels.items():
+        tokens[levelname] = {
+            'root': [
+                # method names
+#                (r'^([ \t]*(?:' + cs_ident + r'(?:\[\])?\s+)+?)' # return type
+#                 r'(' + cs_ident + ')'                           # method name
+#                 r'(\s*)(\()',                               # signature start
+#                 bygroups(using(this), Name.Function, Text, Punctuation)),
+                (r'(function|method)([ \t]+)'
+                 r'(' + cs_ident + r')'
+                 r'(\s*)(\()',                               # signature start
+                 bygroups(Keyword, Text, Name.Function, Text, Punctuation)),
+                (r'[^\S\n]+', Text),
+                (r'\\\n', Text), # line continuation
+                (r'//.*?\n', Comment.Single),
+                (r'/[*].*?[*]/', Comment.Multiline),
+                (r'\n', Text),
+                (r'[~!%^&*()+=|\[\]:;,.<>/?-]', Punctuation),
+                (r'[{}]', Punctuation),
+                 (r'@"(""|[^"])*"', String),
+                (r'"(\\\\|\\"|[^"\n])*["\n]', String),
+                (r"'\\.'|'[^\\]'", String.Char),
+                (r"[0-9](\.[0-9]*)?([eE][+-][0-9]+)?"
+                 r"[flFLdD]?|0[xX][0-9a-fA-F]+[Ll]?", Number),
+                (r'\b(extern)(\s+)(alias)\b', bygroups(Keyword, Text,
+                 Keyword)),
+                (r'(assert|assume|else|ensures|exists|false|forall|'
+                 r'free|ghost|if|in|invariant|new|null|'
+                 r'return|returns|static|this|then|true|requires|var|while)\b', Keyword),
+                (r'(bool|int|nat|seq|set)\b\??', Keyword.Type),
+                (r'(class)(\s+)', bygroups(Keyword, Text), 'class'),
+                (cs_ident, Name),
+                ],
+
+            'class': [
+                (cs_ident, Name.Class, '#pop')
+                ],
+            }
+
+    def __init__(self, **options):
+        level = get_choice_opt(options, 'unicodelevel', self.tokens.keys(), 'basic')
+        if level not in self._all_tokens:
+            # compile the regexes now
+            self._tokens = self.__class__.process_tokendef(level)
+        else:
+            self._tokens = self._all_tokens[level]
+
+        RegexLexer.__init__(self, **options)