Automath Pygments Highlighter

automath.py

from pygments import highlight
from pygments.lexer import RegexLexer, bygroups
from pygments.token import *
from pygments.formatters import HtmlFormatter

# A quick and dirty syntax highlighter for Automath code
# Admittedly, this should be cleaned up some, but it's just a proof of concept.

class AutomathLexer(RegexLexer):
    name = 'Automath'
    aliases = ['aut']
    filenames = ['*.aut']
    identifier = '([a-zA-Z0-9_\'\`]+)'
    semi = '(\'E\'|;|\:)'
    assignment = '(\:=)'
    ws='(\s*)'
    tokens = {
        'root': [
           # include('whitespace'),
            (r'\[\s*'+identifier+'\s*[\:,]\s*'+identifier+'\s*\]', Text),
            #(r"EB|'eb'|---", Keyword.Reserved),
            #(r"PN|'pn'|PRIM|'prim'|\?\?\?", Keyword.Reserved),
            # (r"TYPE|PROP", Name.Builtin),
            (r"[\*@]", Operator),
            # Name.Class : Keyword.Pseudo := Name.Function
            (r''+identifier+ws+semi+ws+identifier+ws+assignment+ws+identifier,
             bygroups(Name.Class, Text, Operator, Text, Keyword.Pseudo, Text, Operator, Text, Name.Function)),
            # Name.Class := Name.Function : Keyword.Pseudo
            (r''+identifier+ws+assignment+ws+identifier+ws+semi+ws+identifier,
             bygroups(Name.Class, Text, Operator, Text, Name.Function, Text, Operator, Text, Keyword.Pseudo)),
            (r''+identifier, Name.Variable),
            (r'\n', Text),
            (r'\s+', Text),
            (r'#.*?\n', Comment), 
           (r'\{[^\}]*\}', Comment.Multiline),
        ],
    }

# Example
code = "{ Multline\nTest }\n* prop : TYPE := PRIM\n* [a:prop] proof : TYPE := PRIM\n* term : TYPE := PRIM"
print highlight(code, AutomathLexer(), HtmlFormatter())