We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
In #2588 , @bafain reports the following:
There seems to be a problem with the LaTeX code generated for multi-line comments that contain blank lines.
Agda version: 2.6.2-292237b XeTeX version: 3.14159265-2.6-0.999991 (TeX Live 2019/Arch Linux) Literate Agda file Test.lagda:
2.6.2-292237b
3.14159265-2.6-0.999991 (TeX Live 2019/Arch Linux)
Test.lagda
\documentclass{article} \usepackage{agda} \begin{document} \begin{code} module Test where {- -} {- A -} {- B B -} {- C C -} \end{code} \end{document}
Generated LaTeX file latex/Test.tex:
latex/Test.tex
[..] \>[0]\AgdaComment{\{- C C -\}}\<% [..]
Error:
$ agda --latex Test.lagda $ cd latex $ xelatex Test.tex [..] Runaway argument? {\textcolor {AgdaComment}{\{- C ! Paragraph ended before \text@command was complete. <to be read again> \par l.34 \end{code} ?
The text was updated successfully, but these errors were encountered:
A fix seems to be:
\AgdaComment
This is basically #2588 (comment) (@nad):
A simple fix might be to extend stringLiteral to handle comments as well.
stringLiteral
Sorry, something went wrong.
[ fix #5398 ] by WYSIWYG for block comments
c93567c
Block comments are now latexed line-by-line, rather than as one paragraph. This solves the problem of empty lines.
[ #5398 ] test case
72030fc
6e4fb9d
b804d6b
andreasabel
Successfully merging a pull request may close this issue.
In #2588 , @bafain reports the following:
There seems to be a problem with the LaTeX code generated for multi-line comments that contain blank lines.
Agda version:
2.6.2-292237b
XeTeX version:
3.14159265-2.6-0.999991 (TeX Live 2019/Arch Linux)
Literate Agda file
Test.lagda
:Generated LaTeX file
latex/Test.tex
:Error:
The text was updated successfully, but these errors were encountered: