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

[Guillermo Calderón]

Hi Jesper,

Thanks for your answer.

Unfortunately, the sequence of commands that you propose doesn't give 
the result that I am asking for.

I try it but

1)  pandoc converts agda  blocks in latex code.
2)  agda latex backend doesn't find any agda block to convert.
3)  In addition, agda.sty doesn't seem to be compatible with latex stuff 
generated by pandoc.

I think that  something like `--html-higligth=code` is required for 
latex backend.

I will create a feature request on the bug tracker.

Best regards,

Guillermo

On 11/8/19 06:35, Jesper Cockx wrote:
> 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 <http://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 
> <mailto:calderon at fing.edu.uy>> wrote:
> 
>     Dear all:
> 
>     If I have a file foo.lagda.md <http://foo.lagda.md>, I can use
>     pandoc to generate a pdf:
> 
>     ```
>     $ pandoc --standalone foo.lagda.md <http://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
>     <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>