How to beamer \alert code snippets in lhs2TeX?

Question

How to highlight particular ranges of lhs2TeX code in beamer?

Naive example (to be preprocessed with lhs2TeX --agda):

\documentclass{beamer}
%include agda.fmt
\begin{document}
\begin{frame}
\begin{spec}
somefunction :  {-"\begin{alertenv}"-}importantaspect{-"\end{alertenv}"-}
                secondline
\end{spec}
\end{frame}
\end{document}

Compiling such a snippet fails with:

./test.tex:308: Incompatible glue units.
\reset@color ->\beamer@lastskip =\lastskip 
                                           \edef \beamer@lastskiptexta {\the...
l.308 \end{frame}

Answer 1

In Agda mode, the alerted region contains an occurrence of \;, as you can observe if you look at the generated code:

\>[17]{}\begin{alertenv}\Varid{importantaspect}\;\end{alertenv}{}\<[E]%

This is triggering the error (it's a muskip and apparently something tries to put it into a normal skip register, leading to the incompatibility error; however, I don't currently completely understand who's responsible). One can argue that lhs2TeX shouldn't put the skip there in the first place.

I can see two workarounds.

(1) Put another skip in that's easier to digest:

somefunction :  {-"\begin{alertenv}"-}importantaspect{-"\hskip0pt\end{alertenv}"-}

(2) Avoid the skip from being inserted by using a different formatting mechanism, for example

%format Importantaspect = "\alert{" importantaspect "}"

and then

somefunction :  Importantaspect