[Agda] How to convert literate agda markdown to pdf with syntax-highligting

[Jesper Cockx]

Hi Guillermo,

There does not seem to be an official way to do this at the moment, but the
following seems to work (at least on a small test file):

```
pandoc --standalone test.lagda.md -o test2.lagda.tex
agda --latex test2.lagda.tex
pdflatex latex/test2.tex
```

Note that you cannot choose the file name `test.lagda.tex` since Agda
detects a conflict between two modules with the same name. Perhaps Agda
could be extended to support this use case in a more native way, feel free
to create a feature request on the bug tracker at
https://github.com/agda/agda/issues.

-- Jesper

On Fri, Aug 9, 2019 at 9:53 PM Guillermo Calderon <calderon at fing.edu.uy>
wrote:

> Dear all:
>
> If I have a file  foo.lagda.md, I can use pandoc to generate a pdf:
>
> ```
> $ pandoc --standalone foo.lagda.md -o foo.langda.pdf
> ```
>
> This works but the agda code is poorly highlighted by pandoc/latex.
>
>
> Is it posible to apply the latex backend of Agda to highlight the code
> in the document?
>
> I so, what would be the approppriate sequence of pandoc/agda  commands
> to obtain this goal?
>
> Thanks in advance.
> Best regards,
>
> Guillermo
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190811/cd7f51f8/attachment.html>