Agda pragmas are rendered incorrectly

[andreasabel]

A pragma like

{-# NO_TERMINATION_CHECK #-}

is rendered in math mode, interpreting _ as subscript. Correct would be a rendering in verbatim mode.

[asr]

Talking about Agda pragmas, the below pragma is wrong indented.

data ℕ : Set where zero : ℕ suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

[kosmikus]

I'm in general not really motivated to handle pragmas. They're also not handled well in Haskell. The correct way to format pragma really differs per pragma, and I don't want to add so many special cases to lhs2TeX.

[asr]

I could fix the indentation problem changing

%subst pragma a = "\mbox{\enskip{-#" a " #-}\enskip}"

to

%subst pragma a = "\mbox{{-#" a " #-}}"

in the file lhs2TeX.fmt.lit. It also fixed the indentation problem for Haskell using the default style. I guess it is also necessary remove \enskip from the line below for other styles.

%subst pragma a = "{\rmfamily\enskip{-#" a " #-}\enskip}"

[kosmikus]

As long as all you need is a changed %subst, there's no need to change/patch lhs2TeX itself. You can just put the directive in your source file, or in a library file that you %include.

[asr]

That is possible, of course! However, why not fix this issue for all the users?

[patrick-nicodemus]

@andreasabel do you have a way to fix this, even a hacky workaround?

[andreasabel]

@patrick-nicodemus : @asr mentions a workaround above, have you tried it?

[patrick-nicodemus]

@andreasabel Yes, I tried it and I was unable to adapt it to my problem. I want to translate

\begin{code}
{-# BUILTIN EQUALITY _≡_ #-}
\end{code}

However I am unable to figure out how to escape the underscores around equality. I tried %format but I had no luck here. When I try

%subst pragma a = "\mbox{{-#\verb|" a "| #-}}"

the code it generates is then passed as an argument to the columns macro, I think, or possibly to another macro ColumnHook (idk how to read this kind of LaTeX code) but either way it is apparently not possible to wrap something in a verbatim environment before passing it to a function - https://tex.stackexchange.com/questions/83893/verbatim-inside-a-command

And \texttt does not escape underscores.

I should note that implicitly opening math mode with an underscore and that not closing it again causes the document to fail to compile. So it is a serious problem, I cannot get a working pdf. The manual says

If you wish to hide code from the compiler, but not from lhs2TEX, you can flip the > characters around.

I was unable to find similar instructions to hide the pragma from lhs2TEX but not the compiler.

[andreasabel]

@patrick-nicodemus You could try and fork lhs2tex and see whether you can implement what you want.
Or use Agda's latex backend (which unfortunately lacks the convenience to format inline code).