4
$\begingroup$

I am making Beamer slides for a talk about an Agda formalisation of mine.

In order to make the code fit onto the slide, I need to scale the font size. One would think that this might not be so hard, but the previous 20 tricks that I've tried all fail in the sense that, post compilation with agda --latex, the relevant tricks simply disappear from the output file.

I tried setting the global document font size to the smallest possible option (and then using \Huge for all remaining text), but 8pt on a Beamer project is still quite large and doesn't quite give me the room that I need.

Has anybody here ever been able to successfully change the code output size in a Literate Agda project?

P.S. There exists at least one absolutely unpalatable solution: hand modifying the output latex files.

$\endgroup$
1
  • $\begingroup$ As it would happen, in the weirdest twist, it turns out that the modifiers \tiny and \scriptsize do affect Agda code while the modifier \small does not (this was what I first attempted)! I would still like for a solution that lets me scale by any numeric factor. $\endgroup$ Mar 27, 2022 at 21:20

1 Answer 1

4
$\begingroup$

This is more of a LaTeX question. All the generated code will typically end up in a code environment and so you can use a LaTeX solution to patch that environment.

Using this answer, I get the following file:

\documentclass[9pt]{article}
\usepackage{agda}

\makeatletter
\g@addto@macro{\code}{\fontsize{15}{18}}\selectfont
\makeatother

\begin{document}

This is not in a code environment

\begin{code}
module LaTeX where
-- this is in a code environment
\end{code}

And we're back out of the code environment

\end{document}

and this is what the output looks like:

Result once compiled

The first argument to fontsize is the actual size, the second is the distance between the bottom of 2 consecutive lines in a paragraph so should probably be ~20% bigger than the first one.

$\endgroup$
2
  • 3
    $\begingroup$ Thank you for the answer! The issue that I'm experiencing with this now is that adding your three lines makes the \begin{code}[hide] optioned variant stop working. $\endgroup$ Mar 27, 2022 at 23:17
  • 2
    $\begingroup$ However using \AtBeginEnvironment{code}{\fontsize{9}{12}\selectfont} does work! $\endgroup$ Mar 27, 2022 at 23:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.