New role ghref for pointing to files on github

alectryon/docutils.py

@@ -752,6 +752,86 @@ def coq_code_role(role, rawtext, text, lineno, inliner,
 
 coq_code_role.name = "coq" # type: ignore
 
+import re
+ghref_cache = {}
+ghref_scrape_re = re.compile("<a(.*?hotkey=.y.*?)>Permalink</a>",re.IGNORECASE)
+ghref_scrape_href_re = re.compile('href=([\'"])(.*?)\\1',re.IGNORECASE)
+def ghref_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
+    src = options.get('src',None)
+    if src is None:
+        msg = inliner.reporter.error("{}: no src option".format(role), line=lineno)
+        return [inliner.problematic(rawtext, rawtext, msg)], [msg]
+    components = str.split(src,sep=" ")
+    if len(components) != 4:
+        msg = inliner.reporter.error("{}: src should be 4 space separated strings".format(role), line=lineno)
+        return [inliner.problematic(rawtext, rawtext, msg)], [msg]
+    org, repo, branch, path = components
+    uri = "https://github.com/{}/{}/blob/{}/{}".format(org,repo,branch,path)
+    roles.set_classes(options)
+    options.setdefault("classes", []).append("ghref")
+    if uri in ghref_cache:
+        code, rawuri, uri = ghref_cache[uri]
+    else:
+        from urllib import request
+        try:
+            with request.urlopen(uri) as f:
+                html = f.read().decode('utf-8')
+        except:
+            msg = inliner.reporter.error("{}: could not download: {}".format(role,uri), line=lineno)
+            return [inliner.problematic(rawtext, rawtext, msg)], [msg]
+        try:
+            link = ghref_scrape_re.search(html).group(1)
+            puri = ghref_scrape_href_re.search(link).group(2)
+        except:
+            msg = inliner.reporter.error("{}: could not scrape for permalink: {}".format(role,uri), line=lineno)
+            return [inliner.problematic(rawtext, rawtext, msg)], [msg]
+        puri = "https://github.com" + puri
+        rawuri = puri.replace('/blob/','/raw/')
+        try:
+            with request.urlopen(rawuri) as f:
+                code = f.read().decode('utf-8')
+        except:
+            msg = inliner.reporter.error("{}: could not download: {}".format(role,rawuri), line=lineno)
+            return [inliner.problematic(rawtext, rawtext, msg)], [msg]
+        ghref_cache[uri]=(code,rawuri,puri)
+        uri=puri
+    mangler = options.get('replace',None)
+    mangler_with = options.get('replace_with','')
+    if mangler is None:
+        name=text
+    else:
+        name = re.sub(mangler,mangler_with,text)
+    pattern = options.get('pattern','')
+    from string import Template
+    pattern = Template(pattern).safe_substitute(name=name)
+    pattern = re.compile(pattern)
+    for num, line in enumerate(code.splitlines(), 1):
+        if pattern.search(line):
+            uri = uri + '#L' + str(num)
+            break
+    else:
+        msg = inliner.reporter.error("{}: {} not found in {} using pattern {}".format(role,text,rawuri,pattern), line=lineno)
+        return [inliner.problematic(rawtext, rawtext, msg)], [msg]
+    node = nodes.reference(rawtext, text, refuri=uri, **options)
+    set_line(node, lineno, inliner.reporter)
+    return [node], []
+ghref_role.name = "ghref"
+ghref_role.options = {
+    # the GH source, 4 fields separated by space: org repo branch path. Eg
+    #   :src: cpitclaudel alectryon master alectryon/docutils.py
+    "src": directives.unchanged,
+    # the regex to find the location in the raw file at path. I must use $name
+    # this is replaced by the text in :ghref:`text`. Eg
+    #   :pattern: ^def $name
+    "pattern": directives.unchanged,
+    # optionally mangle the name before substituting it in the regexp using
+    # re.sub. Eg
+    #   :replace: this
+    #   :replace_with: that
+    "replace": directives.unchanged,
+    "replace_with": directives.unchanged
+}
+
 COQ_ID_RE = re.compile(r"^(?P<title>.*?)(?:\s*<(?P<target>.*)>)?$")
 COQ_IDENT_DB_URLS = [
     ("Coq", "https://coq.inria.fr/library/$modpath.html#$ident")
@@ -1257,7 +1337,8 @@ def get_pipeline(frontend, backend, dialect):
          coq_code_role,
          coq_id_role,
          marker_ref_role,
-         marker_quote_role]
+         marker_quote_role,
+         ghref_role]
 
 def register():
     """Tell Docutils about our roles and directives."""

alectryon/elpi_lexer.py

@@ -0,0 +1,160 @@
+
+"""
+A pygments lexer for Elpi.
+"""
+
+from pygments.lexer import RegexLexer, default, words, bygroups, include, inherit
+from pygments.regexopt import regex_opt, regex_opt_inner
+from pygments.token import \
+    Text, Comment, Operator, Keyword, Name, String, Number
+
+class ElpiLexer(RegexLexer):
+    """
+    For the `Elpi <http://github.com/LPCIC/elpi>`_ programming language.
+
+    .. versionadded:: 1.0
+    """
+
+    name = 'Elpi'
+    aliases = ['elpi']
+    filenames = ['*.elpi']
+    mimetypes = ['text/x-elpi']
+
+    lcase_re = r"[a-z]"
+    ucase_re = r"[A-Z]"
+    digit_re = r"[0-9]"
+    schar2_re = r"(\+|\*|/|\^|<|>|`|'|\?|@|#|~|=|&|!)"
+    schar_re = r"({}|-|\$|_)".format(schar2_re)
+    idchar_re = r"({}|{}|{}|{})".format(lcase_re,ucase_re,digit_re,schar_re)
+    idcharstarns_re = r"({}+|(?=\.[a-z])\.{}+)".format(idchar_re,idchar_re)
+    symbchar_re = r"({}|{}|{}|{}|:)".format(lcase_re, ucase_re, digit_re, schar_re)
+    constant_re = r"({}{}*|{}{}*|{}{}*|_{}+)".format(ucase_re, idchar_re, lcase_re, idcharstarns_re,schar2_re, symbchar_re,idchar_re)
+    symbol_re=r"(,|<=>|->|:-|;|\?-|->|&|=>|as|<|=<|=|==|>=|>|i<|i=<|i>=|i>|is|r<|r=<|r>=|r>|s<|s=<|s>=|s>|@|::|`->|`:|`:=|\^|-|\+|i-|i\+|r-|r\+|/|\*|div|i\*|mod|r\*|~|i~|r~)"
+    escape_re=r"\(({}|{})\)".format(constant_re,symbol_re)
+    const_sym_re = r"({}|{}|{})".format(constant_re,symbol_re,escape_re)
+
+    tokens = {
+        'root': [ include('elpi') ],
+
+        'elpi': [
+
+            include('_elpi-comment'),
+
+            (r"(:before|:after|:if|:name)(\s*)(\")",bygroups(Keyword.ElpiMode,Text,String.Double),'elpi-string'),
+            (r"(:index)(\s*\()",bygroups(Keyword.ElpiMode,Text),'elpi-indexing-expr'),
+            (r"(external pred|pred)(\s+)({})".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-pred-item'),
+            (r"(external type|type)(\s+)(({}(,\s*)?)+)".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-type'),
+            (r"(kind)(\s+)(({}|,)+)".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-type'),
+            (r"(typeabbrev)(\s+)({})".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction),'elpi-type'),
+            (r"(accumulate)(\s+)(\")",bygroups(Keyword.ElpiKeyword,Text,String.Double),'elpi-string'),
+            (r"(accumulate|shorten|namespace|local)(\s+)({})".format(constant_re),bygroups(Keyword.ElpiKeyword,Text,Text)),
+            (r"(pi|sigma)(\s+)([a-zA-Z][A-Za-z0-9_ ]*)(\\)",bygroups(Keyword.ElpiKeyword,Text,Name.ElpiVariable,Text)),
+            (r"rule",Keyword.ElpiKeyword),
+            (r"(constraint)(\s+)(({}(\s+)?)+)".format(const_sym_re),bygroups(Keyword.ElpiKeyword,Text,Name.ElpiFunction)),
+
+            (r"(?=[A-Z_]){}".format(constant_re),Name.ElpiVariable),
+            (r"(?=[a-z_]){}\\".format(constant_re),Name.ElpiVariable),
+            (r"_",Name.ElpiVariable),
+            (r"({}|!|=>|;)".format(symbol_re),Keyword.ElpiKeyword),
+            (constant_re,Text),
+            (r"\[|\]|\||=>",Keyword.ElpiKeyword),
+            (r'"', String.Double, 'elpi-string'),
+            (r'`', String.Double, 'elpi-btick'),
+            (r'\'', String.Double, 'elpi-tick'),
+            (r'\{[^\{]', Text, 'elpi-spill'),
+            (r"\(",Text,'elpi-in-parens'),
+            (r'\d[\d_]*', Number.ElpiInteger),
+            (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.ElpiFloat),
+            (r"[+\*-/\^]", Operator),
+        ],
+        '_elpi-comment': [
+            (r'%[^\n]*\n',Comment),
+            (r'/\*',Comment,'elpi-multiline-comment'),
+            (r"\s+",Text),
+        ],
+        'elpi-multiline-comment': [
+            (r'\*/',Comment,'#pop'),
+            (r'.',Comment)
+        ],
+        'elpi-indexing-expr':[
+            (r'[0-9 _]+',Number.ElpiInteger),
+            (r'\)',Text,'#pop'),
+        ],
+        'elpi-type': [
+            (r"(ctype\s+)(\")",bygroups(Keyword.Type,String.Double),'elpi-string'),
+            (r'->',Keyword.Type),
+            (constant_re,Keyword.Type),
+            (r"\(|\)",Keyword.Type),
+            (r"\.",Text,'#pop'),
+            include('_elpi-comment'),
+        ],
+        'elpi-pred-item': [
+            (r"[io]:",Keyword.ElpiMode,'elpi-ctype'),
+            (r"\.",Text,'#pop'),
+            include('_elpi-comment'),
+        ],
+        'elpi-ctype': [
+            (r"(ctype\s+)(\")",bygroups(Keyword.Type,String.Double),'elpi-string'),
+            (constant_re,Keyword.Type),
+            (r"\(|\)",Keyword.Type),
+            (r",",Text,'#pop'),
+            (r"\.",Text,'#pop:2'),
+            include('_elpi-comment'),
+        ],
+        'elpi-btick': [
+            (r'[^` ]+', String.Double),
+            (r'`', String.Double, '#pop'),
+        ],
+        'elpi-tick': [
+            (r'[^\' ]+', String.Double),
+            (r'\'', String.Double, '#pop'),
+        ],
+        'elpi-string': [
+            (r'[^\"]+', String.Double),
+            (r'"', String.Double, '#pop'),
+        ],
+        'elpi-spill': [
+            (r'\{[^\{]', Text, '#push'),
+            (r'\}[^\}]', Text, '#pop'),
+            include('elpi'),
+        ],
+        'elpi-in-parens': [
+            (r"\(", Operator, '#push'),
+            (r"\)", Operator, '#pop'),
+            include('elpi'),
+        ],
+
+    }
+
+from .pygments_lexer import CoqLexer
+
+class CoqLexer(CoqLexer, ElpiLexer):
+
+    tokens = {
+      'root': [
+            # No clue what inherit would do here, so we copy Coq's ones
+            include('_basic'),
+            include('_vernac'),
+            include('_keywords'),
+            include('_other'),
+      ],
+      '_quotations': [
+            (r"lp:\{\{",Text, 'elpi'),
+            (r"(lp:)([A-Za-z_0-9']+)",bygroups(Text, Name.ElpiVariable)),
+            (r"(lp:)(\()([A-Z][A-Za-z_0-9']*)([a-z0-9 ]+)(\))",bygroups(Text,Text,Name.ElpiVariable,Text,Text)),
+            inherit
+      ],
+      'antiquotation': [
+            (r"\}\}",Text,'#pop'),
+            inherit
+      ],
+      'elpi': [
+            (r"\}\}",Text,'#pop'),
+            (r"global|sort|app|fun|let|prod|match|fix", Keyword.ElpiKeyword),
+            (r"\{\{",Text,'antiquotation'), # back to Coq
+            inherit
+      ],
+
+    }
+
+__all__ = ["ElpiLexer","CoqLexer"]

alectryon/pygments.py

@@ -33,7 +33,7 @@
 
 from dominate.util import raw as dom_raw
 
-from .pygments_lexer import CoqLexer
+from .elpi_lexer import CoqLexer
 from .pygments_style import AlectryonStyle
 
 LEXER = CoqLexer(ensurenl=False) # pylint: disable=no-member
@@ -215,5 +215,6 @@ def replace_builtin_coq_lexer():
     from pygments.lexers import _lexer_cache
     from pygments.lexers._mapping import LEXERS
     (_mod, name, aliases, ext, mime) = LEXERS['CoqLexer']
-    LEXERS['CoqLexer'] = ("alectryon.pygments_lexer", name, aliases, ext, mime)
+    LEXERS['CoqLexer'] = ("alectryon.elpi_lexer", name, aliases, ext, mime)
     _lexer_cache.pop(name, None)
+    LEXERS['ElpiLexer'] = ('alectryon.elpi_lexer','Elpi',('elpi',),('*.elpi',),('text/x-elpi',))

alectryon/pygments_lexer.py

@@ -512,14 +512,19 @@ class CoqLexer(RegexLexer):
             include('_basic'),
             default("#pop"),
         ],
-
+        '_quotations': [
+        ],
+        'antiquotation': [
+            include('_gallina'),
+        ],
         # The symbol regexp below consumes symbol chars one by one.  Without
         # this, expressions like ``("x", y)`` would be incorrectly parsed as
         # ``("``, ``x``, and ``", y)``, with the first ``"`` coalesced with the
         # preceding ``(`` and the second ``"`` lexed as a string opener.
         # Clients can reconstitute multi-character symbols later (e.g. before
         # running other filters) using a ``TokenMergeFilter``.
         '_other': [
+            include('_quotations'),
             (name_re, Name),
             (evar_re, Name.Label),
             # ['] is not a symbol character according to the grammar, but it has
@@ -530,3 +535,4 @@ class CoqLexer(RegexLexer):
     }
 
 __all__ = ["CoqLexer"]
+