Agda support

[youqad]

Hello, thank you for your amazing code highlighter! I'm using it on my Jekyll blog 😃

Would it be possible to add support for Agda? (there's already support for Coq, it's unfair 😝) Its syntax is pretty close to Haskell, but the Haskell highlighting doesn't look that great, especially for (dependent) type signatures:

http://younesse.net/agda-basics/

Thank you very much in advance! 😋

[ice1000]

I wonder if there's any plan to add agda highlight support.

[stale[bot]]

This contribution has been automatically marked as stale because it has not had any activity for more than a year. It will be closed if no additional activity occurs within the next 14 days.

[ice1000]

Oh no! Please don't

[pyrmont]

@ice1000 Thanks for letting us know this is something that's still desired. Unfortunately, I should probably warn that Rouge adds features from the contributions of its members and so whether support for this is added or not really depends on what's submitted. Of course, since Rouge is open source, the good news is that the person to submit the lexer could be you!

When I became a maintainer I put together a guide that tries to explain how you can do that. There's quite a backlog of PRs we're working our way through but we are giving priority to newer ones so if you do submit something, it'll go to the top of the pile :)

[pnlph]

There is already a pygments class, but also for Idris and other haskell-related languages. Is this helping for having a new lexer or it must be built from scratch?

class AgdaLexer(RegexLexer):
    """
    For the `Agda <http://wiki.portal.chalmers.se/agda/pmwiki.php>`_
    dependently typed functional programming language and proof assistant.
    .. versionadded:: 2.0
    """

    name = 'Agda'
    aliases = ['agda']
    filenames = ['*.agda']
    mimetypes = ['text/x-agda']

    reserved = ['abstract', 'codata', 'coinductive', 'constructor', 'data',
                'field', 'forall', 'hiding', 'in', 'inductive', 'infix',
                'infixl', 'infixr', 'instance', 'let', 'mutual', 'open',
                'pattern', 'postulate', 'primitive', 'private',
                'quote', 'quoteGoal', 'quoteTerm',
                'record', 'renaming', 'rewrite', 'syntax', 'tactic',
                'unquote', 'unquoteDecl', 'using', 'where', 'with']

    tokens = {
        'root': [
            # Declaration
            (r'^(\s*)([^\s(){}]+)(\s*)(:)(\s*)',
             bygroups(Text, Name.Function, Text, Operator.Word, Text)),
            # Comments
            (r'--(?![!#$%&*+./<=>?@^|_~:\\]).*?$', Comment.Single),
            (r'\{-', Comment.Multiline, 'comment'),
            # Holes
            (r'\{!', Comment.Directive, 'hole'),
            # Lexemes:
            #  Identifiers
            (r'\b(%s)(?!\')\b' % '|'.join(reserved), Keyword.Reserved),
            (r'(import|module)(\s+)', bygroups(Keyword.Reserved, Text), 'module'),
            (r'\b(Set|Prop)\b', Keyword.Type),
            #  Special Symbols
            (r'(\(|\)|\{|\})', Operator),
            (u'(\\.{1,3}|\\||\u039B|\u2200|\u2192|:|=|->)', Operator.Word),
            #  Numbers
            (r'\d+[eE][+-]?\d+', Number.Float),
            (r'\d+\.\d+([eE][+-]?\d+)?', Number.Float),
            (r'0[xX][\da-fA-F]+', Number.Hex),
            (r'\d+', Number.Integer),
            # Strings
            (r"'", String.Char, 'character'),
            (r'"', String, 'string'),
            (r'[^\s(){}]+', Text),
            (r'\s+?', Text),  # Whitespace
        ],
        'hole': [
            # Holes
            (r'[^!{}]+', Comment.Directive),
            (r'\{!', Comment.Directive, '#push'),
            (r'!\}', Comment.Directive, '#pop'),
            (r'[!{}]', Comment.Directive),
        ],
        'module': [
            (r'\{-', Comment.Multiline, 'comment'),
            (r'[a-zA-Z][\w.]*', Name, '#pop'),
            (r'[\W0-9_]+', Text)
        ],
        'comment': HaskellLexer.tokens['comment'],
        'character': HaskellLexer.tokens['character'],
        'string': HaskellLexer.tokens['string'],
        'escape': HaskellLexer.tokens['escape']
    }

[pyrmont]

@pnlph The Pygments class is helpful as a guide but it's written in Python and Rouge is a Ruby library. It doesn't by itself provide a means to add this functionality; it merely could assist someone writing a lexer in Ruby.

[ayberkt]

I've just learned from GitLab people that this issue is what needs to be resolved to get GitLab to syntax-highlight Agda code.

@pyrmont Is the only thing that's needed an Agda lexer? I will be happy to work on that if it will resolve this issue although I don't know much about Ruby. What is the standard lexer generator for it? It shouldn't be too hard to take Agda's lexer that uses Alex and translate that to the analogous tool for Ruby.

I looked at the guide you linked to but it seems to talk about hand-writing a lexer which is both tedious and error-prone, given that generating a lexer from a lexer specification is a well-automated task.

[pyrmont]

@ayberkt Rouge follows a similar approach to earlier syntax highlighting libraries like Pygments which rely on handwritten lexers. It's true that these can include errors but for the uses Rouge is put to (typically improving the readability of documentation), this hasn't ever been a significant problem. There is no 'standard lexer generator' for Ruby as far as I'm aware.

[ayberkt]

@pyrmont okay then I'll try to adapt the Pygments lexer pointed out by @pnlph. Thanks for the help!