formalism: Use subfiles

formalism/formalism.tex

@@ -1,23 +1,17 @@
 \documentclass{article}
-\input{preamble/preamble}
-\usepackage[margin=1in]{geometry}
 
-\makeatletter
-\renewcommand\tableofcontents{%
-    \@starttoc{toc}%
-}
-\makeatother
+\input{preamble/preamble}
+\usepackage{subfiles}
 
 \begin{document}
-\setcounter{tocdepth}{2}
 \tableofcontents
 
 \renewcommand{\thesection}{\Alph{section}}
 
-\input{marked}
+\subfile{marked}
 \newpage
-\input{untyped}
+\subfile{untyped}
 \newpage
-\input{typed}
+\subfile{typed}
 
 \end{document}

formalism/marked.tex

@@ -1,3 +1,6 @@
+\documentclass[formalism.tex]{subfiles}
+
+\begin{document}
 \section{Marked Lambda Calculus}
 The \emph{marked lambda calculus} is a judgmental framework for bidirectional type error
 localization and recovery. Below is the complete formalization of the calculus on a gradually typed
@@ -953,3 +956,5 @@ \subsubsection{Localize to First}
 
 \input{patterned}
 \input{polymorphism}
+
+\end{document}

formalism/preamble/preamble.tex

@@ -1,3 +1,5 @@
+\hbadness=99999
+
 \usepackage{iftex}
 \ifPDFTeX
   \usepackage{libertinust1math}
@@ -7,6 +9,8 @@
 \fi
 \usepackage[scaled=0.8]{FiraMono}
 
+\usepackage[margin=1in]{geometry}
+
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{amsfonts}
@@ -15,6 +19,8 @@
 \usepackage{mathtools}
 \usepackage{mathpartir}
 \usepackage{stmaryrd}
+\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n}
+
 \usepackage{bm}
 \usepackage{relsize}
 \usepackage{centernot}
@@ -32,3 +38,10 @@
 \declaretheorem[name=Definition, parent=section, style=definition]{definition}
 
 \input{preamble/symbols}
+
+\makeatletter
+\renewcommand\tableofcontents{%
+    \@starttoc{toc}%
+}
+\makeatother
+\setcounter{tocdepth}{2}

formalism/typed.tex

@@ -1,3 +1,6 @@
+\documentclass[formalism.tex]{subfiles}
+
+\begin{document}
 \section{Typed Hazelnut}
 
 \subsection{Syntax}
@@ -116,6 +119,7 @@ \subsubsection{Type Cursor Erasure}
 \subsubsection{Expression Cursor Erasure}
 \judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows:
 %
+\newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}}
 \[\begin{array}{rcl}
   \cursorErasesToRow{\ZCursor{\ECMV}}{\ECMV} \\
   \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{\cursorErase{\ZTMV}}{\ECMV}} \\
@@ -937,3 +941,5 @@ \subsubsection{Metatheorems}
       $\AAEActionIter{\ctx}{\ZMV}{\ZMV''}{\TMV}{\AMV}$, then $\ZMV' = \ZMV''$.
   \end{enumerate}
 \end{theorem}
+
+\end{document}

formalism/untyped.tex

@@ -1,3 +1,6 @@
+\documentclass[formalism.tex]{subfiles}
+
+\begin{document}
 \section{Untyped Hazelnut}
 
 \subsection{Syntax}
@@ -692,3 +695,5 @@ \subsubsection{Metatheorems}
       % $\AUEAction{\ZCursor{\EMV}}{\ZMV}{\AMV}$.
   % \end{enumerate}
 % \end{theorem}
+
+\end{document}