LaTeX backend: italics correction

[ajrouvoet]

The LaTeX backend has an issue with the italics used for bound variables. Usually, if one switches from an italic to a upright font, one has to take care that an italics correction (\/ is the TeX command) is inserted to prevent overlapping characters. The LaTeX macro \textit{..} does this automatically.
It seems however that despite agda.sty using \textit, the correction is often not correctly inserted. This leads to some very common typesetting errors in Agda papers. Below are some examples:

I have no idea if there is a feasible way for the backend to address this.

[andreasabel]

Can this be handled on the level of agda.sty?

[ajrouvoet]

I'm unsure why it happens at all. My feeling is that it is because of the nesting of different style commands, but I've tried modifying agda.sty in different ways and couldn't make it work yet.

[andreasabel]

MWE:

\documentclass{article}
\usepackage{agda}

\begin{document}
Look for missing italics correction \verb|\/| in the following rendering:
\begin{code}
postulate
  id : forall {Γ} {I : Set Γ} (i : I) → I
\end{code}
\end{document}

[andreasabel]

A workaround in case of the MWE is:

\renewcommand{\AgdaBound}[1]{\textit{#1}}

The automatic italics correction \/ tries to analyse when to insert the space but fails if \textcolor is wrapped around the italic text:

\documentclass{article}
\usepackage{agda}

\newcommand{\thecode}{
\begin{code}
postulate _ : forall {Γ} {I : Set Γ} (i : I) → I
\end{code}
}

\begin{document}
Look for missing italics correction \verb|\/| in the following
rendering:
\thecode
{\renewcommand{\AgdaBound}[1]{\textit{#1}}
Fixed with \verb|\renewcommand{\AgdaBound}[1]{\textit{#1}}|:
\thecode}
{\renewcommand{\AgdaBound}[1]{\textit{\textcolor{AgdaBound}{#1}}}
Broken with \verb|\textit{\textcolor{AgdaBound}{#1}}|:
\thecode}
\end{document}

Issue5471.pdf

It seems like swapping the wrappers for color and style would do the job, but there could be collateral damage. Not sure how to test this efficiently...

[ajrouvoet]

From a quick glance over a draft it appears that swapping the style and color indeed does the job 👍 This surprises me, because I thought only face modifiers would affect the italics insertion.

Note that several of the classes are affected (at least AgdaGeneralizable, and AgdaArgument).

[andreasabel]

From a quick glance over a draft it appears that swapping the style and color indeed does the job

Then let's believe (as long as we can) that miracles can still happen... ;-)

[andreasabel]

@ajrouvoet If you have a PR, let me know, I am currently side tracked by other issues. Otherwise, I will return to make a PR later.

[andreasabel]

Ok, I get to it now...

[ajrouvoet]

Thanks @andreasabel for the fix; this will improve a lot of future Agda papers :)

I'll compile my drafts and thesis with this agda.sty for testing.

[nad]

Not sure how to test this efficiently...

When I have made changes that should not affect the output of the LaTeX backend I've used the following script:

#!/bin/sh

OLD_DIR=old
NEW_DIR=new

rm -f $OLD_DIR/agda.sty $NEW_DIR/agda.sty

OLD_AGDA=$1
NEW_AGDA=$2
BASENAME=$(basename $(basename $3 .tex) .lagda)

$OLD_AGDA --latex --latex-dir=$OLD_DIR $3
$NEW_AGDA --latex --latex-dir=$NEW_DIR $3

(cd $OLD_DIR && latexmk -xelatex $BASENAME.tex)
(cd $NEW_DIR && latexmk -xelatex $BASENAME.tex)

comparepdf --compare=appearance $OLD_DIR/$BASENAME.pdf $NEW_DIR/$BASENAME.pdf || \
  diffpdf --appearance $OLD_DIR/$BASENAME.pdf $NEW_DIR/$BASENAME.pdf

I suppose one can invoke it by going to test/LaTeXAndHTML/succeed/ and running something like for FILE in <files to be tested>; do <script> <old Agda> <new Agda> $FILE; done. I've used comparepdf and diffpdf, which were easy to install under Ubuntu.

[ajrouvoet]

FWIW: I have not come across anything out of the ordinary in the output of my thesis. Most importantly, italics correction now appears to work consistently.