Add lexer for Boogie

3 files changed, 49 insertions, 4 deletions

diff --git a/pygments/formatters/_mapping.py b/pygments/formatters/_mapping.py
index 678c069d..bc4d606e 100755
--- a/pygments/formatters/_mapping.py
+++ b/pygments/formatters/_mapping.py
@@ -32,7 +32,6 @@ FORMATTERS = {
     'TestcaseFormatter': ('pygments.formatters.other', 'Testcase', ('testcase',), (), 'Format tokens as appropriate for a new testcase.')
 }
 
-
 if __name__ == '__main__':  # pragma: no cover
     import sys
     import os
diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py
index 05ada4f3..a0071ac9 100644
--- a/pygments/lexers/_mapping.py
+++ b/pygments/lexers/_mapping.py
@@ -49,6 +49,7 @@ LEXERS = {
     'BlitzBasicLexer': ('pygments.lexers.basic', 'BlitzBasic', ('blitzbasic', 'b3d', 'bplus'), ('*.bb', '*.decls'), ('text/x-bb',)),
     'BlitzMaxLexer': ('pygments.lexers.basic', 'BlitzMax', ('blitzmax', 'bmax'), ('*.bmx',), ('text/x-bmx',)),
     'BooLexer': ('pygments.lexers.dotnet', 'Boo', ('boo',), ('*.boo',), ('text/x-boo',)),
+    'BoogieLexer': ('pygments.lexers.esoteric', 'Boogie', ('boogie',), ('*.bpl',), ()),
     'BrainfuckLexer': ('pygments.lexers.esoteric', 'Brainfuck', ('brainfuck', 'bf'), ('*.bf', '*.b'), ('application/x-brainfuck',)),
     'BroLexer': ('pygments.lexers.dsls', 'Bro', ('bro',), ('*.bro',), ()),
     'BugsLexer': ('pygments.lexers.modeling', 'BUGS', ('bugs', 'winbugs', 'openbugs'), ('*.bug',), ()),
diff --git a/pygments/lexers/esoteric.py b/pygments/lexers/esoteric.py
index 7a026aed..3f3e3015 100644
--- a/pygments/lexers/esoteric.py
+++ b/pygments/lexers/esoteric.py
@@ -9,11 +9,11 @@
     :license: BSD, see LICENSE for details.
 """
 
-from pygments.lexer import RegexLexer, include
+from pygments.lexer import RegexLexer, include, words
 from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
-    Number, Punctuation, Error
+    Number, Punctuation, Error, Whitespace
 
-__all__ = ['BrainfuckLexer', 'BefungeLexer', 'RedcodeLexer']
+__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer']
 
 
 class BrainfuckLexer(RegexLexer):
@@ -112,3 +112,48 @@ class RedcodeLexer(RegexLexer):
             (r'[-+]?\d+', Number.Integer),
         ],
     }
+
+
+class BoogieLexer(RegexLexer):
+    """
+    For `Boogie <https://boogie.codeplex.com/>`_ source code.
+
+    .. versionadded:: 2.0
+    """
+    name = 'Boogie'
+    aliases = ['boogie']
+    filenames = ['*.bpl']
+
+    tokens = {
+        'root': [
+            # Whitespace and Comments
+            (r'\n', Whitespace),
+            (r'\s+', Whitespace),
+            (r'//[/!](.*?)\n', Comment.Doc),
+            (r'//(.*?)\n', Comment.Single),
+            (r'/\*', Comment.Multiline, 'comment'),
+
+            (words((
+                'axiom', 'break', 'call', 'ensures', 'else', 'exists', 'function',
+                'forall', 'if', 'invariant', 'modifies', 'procedure',  'requires',
+                'then', 'var', 'while'),
+             suffix=r'\b'), Keyword),
+            (words(('const',), suffix=r'\b'), Keyword.Reserved),
+
+            (words(('bool', 'int', 'ref'), suffix=r'\b'), Keyword.Type),
+            include('numbers'),
+            (r"(>=|<=|:=|!=|==>|&&|\|\||[+/\-=>*<\[\]])", Operator),
+            (r"([{}():;,.])", Punctuation),
+            # Identifier
+            (r'[a-zA-Z_]\w*', Name),
+        ],
+        'comment': [
+            (r'[^*/]+', Comment.Multiline),
+            (r'/\*', Comment.Multiline, '#push'),
+            (r'\*/', Comment.Multiline, '#pop'),
+            (r'[*/]', Comment.Multiline),
+        ],
+        'numbers': [
+            (r'[0-9]+', Number.Integer),
+        ],
+    }