be able to highlight inline Agda code

[divipp]

It would be nice to be able to highlight inline Agda code approximately.
This would be used in literate Agda code.

There is an approximate Agda syntax highlighter in the skylighting Haskell package, but there could be also an approximate guess whether an identifier is a constructor or not too.

Example (suppose that markdown comments are supported, which is a separate issue):

\begin{code}
data A : Set where
    a : A
    b : A
\end{code}

Constructors `a` and `b` ... variables or functions `f` and `g` ...

a should be highlighted with different color than f in the printed output.

This issue is standalone part of a more ambitious plan to integrate pandoc and Agda. The ultimate goal is to be able to present Agda code easily (pandoc supports several output formats, including beamer slides and a few html presentation styles).

[gallais]

Note that there is already something a bit similar in the latex backend. Cf. the wiki

Semi-automatically typesetting inline code

Since Agda version 2.4.2 there is experimental support for semi-automatically typesetting code inside text, using the references option. Here is a full example.

Example.lagda

\documentclass{article}
\usepackage[references]{agda} 
\begin{document}

Here we postulate \AgdaRef{apa}.

\begin{code}
postulate apa : Set
\end{code}

\end{document}