Skip to content

Commit

Permalink
Add a Pygments lexer for the Alt-Ergo language
Browse files Browse the repository at this point in the history
This patch adds a custom Pygments lexer for the Alt-Ergo language and
uses it to make the Sphinx documentation prettier.
  • Loading branch information
bclement-ocp committed Oct 5, 2023
1 parent 0700dea commit b7bc2b9
Show file tree
Hide file tree
Showing 3 changed files with 89 additions and 4 deletions.
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -41,5 +41,8 @@ alt-ergo.js
alt-ergo-worker.js
www/

# Generated python files
__pycache__

# Generated nix files
/result*
72 changes: 72 additions & 0 deletions docs/sphinx_docs/alt_ergo_lexer.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
from pygments.lexer import RegexLexer, include
from pygments.token import *

__globals__ = [ 'AltErgoLexer' ]

class AltErgoLexer(RegexLexer):
"""
For the Alt-Ergo language.
"""

name = 'Alt-Ergo'
url = 'https://alt-ergo.ocamlpro.com/'
aliases = ['alt-ergo']
filenames = ['*.ae']
mimetypes = ['text/x-alt-ergo']

keywords = (
'ac', 'axiom', 'bitv', 'case_split', 'check', 'cut',
'distinct', 'else', 'end', 'exists', 'extends', 'forall',
'function', 'goal', 'check_sat', 'if', 'let', 'logic', 'not',
'predicate', 'prop', 'rewriting', 'then', 'theory',
'type', 'match', 'with', 'of',
)
keyopts = (
r',', r';', r'\(', r'\)', r':', r'->', r'<-', r'<->', r'=', r'<', r'<=',
r'>', r'>=', r'<>', r'\+', r'-', r'\*', r'\*\*', r'\*\*\.', r'/', r'%',
r'@', r'\.', r'#', r'\[', r'\]', r'\{', r'\}', 'r\|', r'\^', r'\|->',
)

word_operators = ('and', 'in', 'or', 'xor')
primitives = ('bool', 'int', 'real', 'unit', 'void')

tokens = {
'escape-sequence': [
(r'\\[\\"\'ntbr]', String.Escape),
(r'\\[0-9]{3}', String.Escape),
(r'\\x[0-9a-fA-F]{2}', String.Escape),
],
'root': [
(r'\s+', Text),
(r'false|true', Name.Builtin.Pseudo),
(r'\(\*(?![)])', Comment, 'comment'),
(r'\b(%s)\b' % '|'.join(keywords), Keyword),
(r'(%s)' % '|'.join(keyopts[::-1]), Operator),
(r'\b(%s)\b' % '|'.join(word_operators), Operator.Word),
(r'\b(%s)\b' % '|'.join(primitives), Keyword.Type),

(r"\??[^\W\d][\w?']*", Name),

(r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),
(r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex),
(r'0[oO][0-7][0-7_]*', Number.Oct),
(r'0[bB][01][01_]*', Number.Bin),
(r'\d[\d_]*', Number.Integer),

(r"'", Keyword),

(r'"', String.Double, 'string'),
],
'comment': [
(r'[^(*)]+', Comment),
(r'\(\*', Comment, '#push'),
(r'\*\)', Comment, '#pop'),
(r'[(*)]', Comment),
],
'string': [
(r'[^\\"]+', String.Double),
include('escape-sequence'),
(r'\\\n', String.Double),
(r'"', String.Double, '#pop'),
],
}
18 changes: 14 additions & 4 deletions docs/sphinx_docs/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@
# If extensions (or modules to document with autodoc) are in another directory,
# add these directories to sys.path here. If the directory is relative to the
# documentation root, use os.path.abspath to make it absolute, like shown here.
#
# import os
# import sys
# sys.path.insert(0, os.path.abspath('.'))

import os
import sys
sys.path.insert(0, os.path.abspath('.'))


# -- Project information -----------------------------------------------------
Expand All @@ -21,6 +21,16 @@
copyright = '2020 - 2023, Alt-Ergo developers'
author = 'Alt-Ergo developers'

# -- Custom lexer ------------------------------------------------------------

# Import our custom lexer
from alt_ergo_lexer import AltErgoLexer
from sphinx.highlighting import lexers
lexers['alt-ergo'] = AltErgoLexer()

# Use alt-ergo as the default language
highlight_language = 'alt-ergo'

# -- Entry point -------------------------------------------------------------

master_doc = 'index'
Expand Down

0 comments on commit b7bc2b9

Please sign in to comment.