<div dir="ltr"><div>Hi Guillermo,</div><div><br></div><div>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):</div><div><br></div><div>```</div><div>pandoc --standalone <a href="http://test.lagda.md">test.lagda.md</a> -o test2.lagda.tex</div><div>agda --latex test2.lagda.tex</div><div>pdflatex latex/test2.tex</div><div>```</div><div><br></div><div>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 <a href="https://github.com/agda/agda/issues">https://github.com/agda/agda/issues</a>.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 9, 2019 at 9:53 PM Guillermo Calderon <<a href="mailto:calderon@fing.edu.uy">calderon@fing.edu.uy</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all:<br>
<br>
If I have a file  <a href="http://foo.lagda.md" rel="noreferrer" target="_blank">foo.lagda.md</a>, I can use pandoc to generate a pdf:<br>
<br>
```<br>
$ pandoc --standalone <a href="http://foo.lagda.md" rel="noreferrer" target="_blank">foo.lagda.md</a> -o foo.langda.pdf<br>
```<br>
<br>
This works but the agda code is poorly highlighted by pandoc/latex.<br>
<br>
<br>
Is it posible to apply the latex backend of Agda to highlight the code <br>
in the document?<br>
<br>
I so, what would be the approppriate sequence of pandoc/agda  commands <br>
to obtain this goal?<br>
<br>
Thanks in advance.<br>
Best regards,<br>
<br>
Guillermo<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>