From e32b21057c384fdd8684aa049402e3f22137c913 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <2206578+carlostome@users.noreply.github.com>
Date: Fri, 24 Jan 2025 18:24:43 +0100
Subject: [PATCH] Fix indentation of record fields in PDF (#651)

* This affects Figures 17 and 44
---
 src/Ledger/Enact.lagda       | 4 ++--
 src/Ledger/Transaction.lagda | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Ledger/Enact.lagda b/src/Ledger/Enact.lagda
index 5a7a93507..9b6e2bc48 100644
--- a/src/Ledger/Enact.lagda
+++ b/src/Ledger/Enact.lagda
@@ -31,7 +31,7 @@ Note that all other fields of \EnactState also contain a \GovActionID
 since they are \HashProtected.
 
 \begin{figure*}[h]
-\begin{AgdaSuppressSpace}
+\begin{AgdaMultiCode}
 \begin{code}
 record EnactEnv : Type where
 \end{code}
@@ -90,7 +90,7 @@ data
 \begin{code}
   _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type
 \end{code}
-\end{AgdaSuppressSpace}
+\end{AgdaMultiCode}
 \caption{Types and function used for the ENACT transition system}
 \label{fig:enact-defs}
 \end{figure*}
diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda
index bbad3a60c..900774bb5 100644
--- a/src/Ledger/Transaction.lagda
+++ b/src/Ledger/Transaction.lagda
@@ -61,7 +61,6 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 
 \begin{figure*}[h]
 \emph{Abstract types}
-\begin{AgdaMultiCode}
 \begin{code}
         Ix TxId AuxiliaryData : Type
 \end{code}
@@ -110,7 +109,6 @@ Ingredients of the transaction body introduced in the Conway era are the followi
   open GovernanceActions hiding (Vote; yes; no; abstain) public
 
   open import Ledger.Certs govStructure using (DCert)
-
 \end{code}
 \begin{NoConway}
 \emph{Derived types}
@@ -126,6 +124,7 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 \end{code}
 \end{NoConway}
 \emph{Transaction types}
+\begin{AgdaMultiCode}
 \begin{code}
   record TxBody : Type where
 \end{code}