Open patrikja opened 10 years ago
Yes, this is a bug.
Actually, I'm not sure how implicit formatting should work in Agda mode. Do you have any concrete suggestions? Is the Haskell-mode behaviour desirable in Agda mode? In Haskell mode, implicit formats of the form identifiersubscript are allowed, but it feels strange to allow these in Agda mode, because has a special meaning there ...
It certainly shouldn't cause loops or stack overflows, I agree :)
Thanks for the report.
Actually, I just discovered that this is a general problem if you try to implicitly format anything that's not recognized properly. So even in Haskell mode, the definition and use of the following formatting directive causes a stack overflow:
%format abc
cat > bug.lagda <<END %include lhs2TeX.fmt %format a1 \begin{code} a1 \end{code} END lhs2TeX --agda bug.lagda > bug.tex
Stack space overflow: current size 8388608 bytes. Use `+RTS -Ksize -RTS' to increase it.
My current work-around is to not use implicit formatting, but it took a while to realise what the problem was.
/Patrik
PS. version 1.18.1 and the same result when buidling from source today.