coqdomain.py 文件源码

def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
    """An inline role to declare grammar productions that are not in fact included
    in a `productionlist` directive.

    Useful to informally introduce a production, as part of running text
    """
    #pylint: disable=dangerous-default-value, unused-argument
    env = inliner.document.settings.env
    targetid = 'grammar-token-{}'.format(text)
    target = nodes.target('', '', ids=[targetid])
    inliner.document.note_explicit_target(target)
    code = nodes.literal(rawtext, text, role=typ.lower())
    node = nodes.inline(rawtext, '', target, code, classes=['inline-grammar-production'])
    set_role_source_info(inliner, lineno, node)
    env.domaindata['std']['objects']['token', text] = env.docname, targetid
    return [node], []