\documentclass[10pt,a4paper]{article}

% Packages
\usepackage{fancyhdr}           % For header and footer
\usepackage{multicol}           % Allows multicols in tables
\usepackage{tabularx}           % Intelligent column widths
\usepackage{tabulary}           % Used in header and footer
\usepackage{hhline}             % Border under tables
\usepackage{graphicx}           % For images
\usepackage{xcolor}             % For hex colours
%\usepackage[utf8x]{inputenc}    % For unicode character support
\usepackage[T1]{fontenc}        % Without this we get weird character replacements
\usepackage{colortbl}           % For coloured tables
\usepackage{setspace}           % For line height
\usepackage{lastpage}           % Needed for total page number
\usepackage{seqsplit}           % Splits long words.
%\usepackage{opensans}          % Can't make this work so far. Shame. Would be lovely.
\usepackage[normalem]{ulem}     % For underlining links
% Most of the following are not required for the majority
% of cheat sheets but are needed for some symbol support.
\usepackage{amsmath}            % Symbols
\usepackage{MnSymbol}           % Symbols
\usepackage{wasysym}            % Symbols
%\usepackage[english,german,french,spanish,italian]{babel}              % Languages

% Document Info
\author{{[}deleted{]}}
\pdfinfo{
  /Title (agda-emacs.pdf)
  /Creator (Cheatography)
  /Author ({[}deleted{]})
  /Subject (Agda Emacs Cheat Sheet)
}

% Lengths and widths
\addtolength{\textwidth}{6cm}
\addtolength{\textheight}{-1cm}
\addtolength{\hoffset}{-3cm}
\addtolength{\voffset}{-2cm}
\setlength{\tabcolsep}{0.2cm} % Space between columns
\setlength{\headsep}{-12pt} % Reduce space between header and content
\setlength{\headheight}{85pt} % If less, LaTeX automatically increases it
\renewcommand{\footrulewidth}{0pt} % Remove footer line
\renewcommand{\headrulewidth}{0pt} % Remove header line
\renewcommand{\seqinsert}{\ifmmode\allowbreak\else\-\fi} % Hyphens in seqsplit
% This two commands together give roughly
% the right line height in the tables
\renewcommand{\arraystretch}{1.3}
\onehalfspacing

% Commands
\newcommand{\SetRowColor}[1]{\noalign{\gdef\RowColorName{#1}}\rowcolor{\RowColorName}} % Shortcut for row colour
\newcommand{\mymulticolumn}[3]{\multicolumn{#1}{>{\columncolor{\RowColorName}}#2}{#3}} % For coloured multi-cols
\newcolumntype{x}[1]{>{\raggedright}p{#1}} % New column types for ragged-right paragraph columns
\newcommand{\tn}{\tabularnewline} % Required as custom column type in use

% Font and Colours
\definecolor{HeadBackground}{HTML}{333333}
\definecolor{FootBackground}{HTML}{666666}
\definecolor{TextColor}{HTML}{333333}
\definecolor{DarkBackground}{HTML}{006FFF}
\definecolor{LightBackground}{HTML}{EFF6FF}
\renewcommand{\familydefault}{\sfdefault}
\color{TextColor}

% Header and Footer
\pagestyle{fancy}
\fancyhead{} % Set header to blank
\fancyfoot{} % Set footer to blank
\fancyhead[L]{
\noindent
\begin{multicols}{3}
\begin{tabulary}{5.8cm}{C}
    \SetRowColor{DarkBackground}
    \vspace{-7pt}
    {\parbox{\dimexpr\textwidth-2\fboxsep\relax}{\noindent
        \hspace*{-6pt}\includegraphics[width=5.8cm]{/web/www.cheatography.com/public/images/cheatography_logo.pdf}}
    }
\end{tabulary}
\columnbreak
\begin{tabulary}{11cm}{L}
    \vspace{-2pt}\large{\bf{\textcolor{DarkBackground}{\textrm{Agda Emacs Cheat Sheet}}}} \\
    \normalsize{by \textcolor{DarkBackground}{{[}deleted{]}} via \textcolor{DarkBackground}{\uline{cheatography.com/40203/cs/12389/}}}
\end{tabulary}
\end{multicols}}

\fancyfoot[L]{ \footnotesize
\noindent
\begin{multicols}{3}
\begin{tabulary}{5.8cm}{LL}
  \SetRowColor{FootBackground}
  \mymulticolumn{2}{p{5.377cm}}{\bf\textcolor{white}{Cheatographer}}  \\
  \vspace{-2pt}{[}deleted{]} \\
  \uline{cheatography.com/deleted-40203} \\
  \end{tabulary}
\vfill
\columnbreak
\begin{tabulary}{5.8cm}{L}
  \SetRowColor{FootBackground}
  \mymulticolumn{1}{p{5.377cm}}{\bf\textcolor{white}{Cheat Sheet}}  \\
   \vspace{-2pt}Published 30th July, 2017.\\
   Updated 30th July, 2017.\\
   Page {\thepage} of \pageref{LastPage}.
\end{tabulary}
\vfill
\columnbreak
\begin{tabulary}{5.8cm}{L}
  \SetRowColor{FootBackground}
  \mymulticolumn{1}{p{5.377cm}}{\bf\textcolor{white}{Sponsor}}  \\
  \SetRowColor{white}
  \vspace{-5pt}
  %\includegraphics[width=48px,height=48px]{dave.jpeg}
  Measure your website readability!\\
  www.readability-score.com
\end{tabulary}
\end{multicols}}




\begin{document}
\raggedright
\raggedcolumns

% Set font size to small. Switch to any value
% from this page to resize cheat sheet text:
% www.emerson.emory.edu/services/latex/latex_169.html
\footnotesize % Small font.

\begin{multicols*}{2}

\begin{tabularx}{8.4cm}{x{2.4 cm} x{5.6 cm} }
\SetRowColor{DarkBackground}
\mymulticolumn{2}{x{8.4cm}}{\bf\textcolor{white}{Global Context}}  \tn
% Row 0
\SetRowColor{LightBackground}
`C-c C-l` & {\bf{L}}oad file \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
`C-c C-x C-c` & {\bf{C}}ompile file \tn 
% Row Count 3 (+ 2)
% Row 2
\SetRowColor{LightBackground}
`C-c C-x C-q` & {\bf{Q}}uit, kill the Agda process \tn 
% Row Count 5 (+ 2)
% Row 3
\SetRowColor{white}
`C-c C-x C-r` & Kill and {\bf{r}}estart the Agda process \tn 
% Row Count 7 (+ 2)
% Row 4
\SetRowColor{LightBackground}
`C-c C-x C-d` & Remove goals and highlighting ({\bf{d}}eactivate) \tn 
% Row Count 9 (+ 2)
% Row 5
\SetRowColor{white}
`C-c C-x C-h` & Toggle display of {\bf{h}}idden arguments \tn 
% Row Count 11 (+ 2)
% Row 6
\SetRowColor{LightBackground}
`C-c C-=` & Show constraints \tn 
% Row Count 12 (+ 1)
% Row 7
\SetRowColor{white}
`C-c C-s` & {\bf{S}}olve constraints \tn 
% Row Count 13 (+ 1)
% Row 8
\SetRowColor{LightBackground}
`C-c C-?` & Show all goals \tn 
% Row Count 14 (+ 1)
% Row 9
\SetRowColor{white}
`C-c C-f` & Move to next goal ({\bf{f}}orward) \tn 
% Row Count 16 (+ 2)
% Row 10
\SetRowColor{LightBackground}
`C-c C-b` & Move to previous goal ({\bf{b}}ackwards) \tn 
% Row Count 18 (+ 2)
% Row 11
\SetRowColor{white}
`C-c C-d` & Infer ({\bf{d}}educe) type \tn 
% Row Count 19 (+ 1)
% Row 12
\SetRowColor{LightBackground}
`C-c C-o` & Module c{\bf{o}}ntents \tn 
% Row Count 20 (+ 1)
% Row 13
\SetRowColor{white}
`C-c C-z` & Search through definitions in scope \tn 
% Row Count 22 (+ 2)
% Row 14
\SetRowColor{LightBackground}
`C-c C-n` & Compute {\bf{n}}ormal form \tn 
% Row Count 23 (+ 1)
% Row 15
\SetRowColor{white}
`C-u C-c C-n` & Compute normal form, ignoring `abstract` \tn 
% Row Count 25 (+ 2)
% Row 16
\SetRowColor{LightBackground}
`C-u C-u C-c C-n` & Compute and print normal form of `show \textless{}expression\textgreater{}` \tn 
% Row Count 27 (+ 2)
% Row 17
\SetRowColor{white}
`C-c C-x M-;` & Comment/uncomment rest of buffer \tn 
% Row Count 29 (+ 2)
% Row 18
\SetRowColor{LightBackground}
`C-c C-x C-s` & Switch to a different Agda version \tn 
% Row Count 31 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}--}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{x{3.52 cm} x{4.48 cm} }
\SetRowColor{DarkBackground}
\mymulticolumn{2}{x{8.4cm}}{\bf\textcolor{white}{Input}}  \tn
% Row 0
\SetRowColor{LightBackground}
`M-x \seqsplit{describe-input-method} Agda` & View all characters you can input using the Agda input method \tn 
% Row Count 3 (+ 3)
% Row 1
\SetRowColor{white}
`C-x 8 RET` & Input unicode by symbol description \tn 
% Row Count 5 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}--}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{x{2.4 cm} x{5.6 cm} }
\SetRowColor{DarkBackground}
\mymulticolumn{2}{x{8.4cm}}{\bf\textcolor{white}{Goal Context}}  \tn
% Row 0
\SetRowColor{LightBackground}
`C-c C-SPC` & Give (fill goal) \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
`C-c C-r` & {\bf{R}}efine. Partial give: makes new holes for missing arguments \tn 
% Row Count 4 (+ 3)
% Row 2
\SetRowColor{LightBackground}
`C-c C-a` & Automatic Proof Search (Auto) \tn 
% Row Count 6 (+ 2)
% Row 3
\SetRowColor{white}
`C-c C-c` & {\bf{C}}ase split \tn 
% Row Count 7 (+ 1)
% Row 4
\SetRowColor{LightBackground}
`C-c C-h` & Compute type of {\bf{h}}elper function and add type signature to kill ring (clipboard) \tn 
% Row Count 10 (+ 3)
% Row 5
\SetRowColor{white}
`C-c C-t` & Goal type \tn 
% Row Count 11 (+ 1)
% Row 6
\SetRowColor{LightBackground}
`C-c C-e` & Context ({\bf{e}}nvironment) \tn 
% Row Count 12 (+ 1)
% Row 7
\SetRowColor{white}
`C-c C-d` & Infer ({\bf{d}}educe) type \tn 
% Row Count 13 (+ 1)
% Row 8
\SetRowColor{LightBackground}
`C-c C-,` & Goal type and context \tn 
% Row Count 14 (+ 1)
% Row 9
\SetRowColor{white}
`C-c C-.` & Goal type, context and inferred type \tn 
% Row Count 16 (+ 2)
% Row 10
\SetRowColor{LightBackground}
`C-c C-o` & Module c{\bf{o}}ntents \tn 
% Row Count 17 (+ 1)
% Row 11
\SetRowColor{white}
`C-c C-n` & Compute {\bf{n}}ormal form \tn 
% Row Count 18 (+ 1)
% Row 12
\SetRowColor{LightBackground}
`C-u C-c C-n` & Compute normal form, ignoring `abstract` \tn 
% Row Count 20 (+ 2)
% Row 13
\SetRowColor{white}
`C-u C-u C-c C-n` & Compute and print normal form of `show \textless{}expression\textgreater{}` \tn 
% Row Count 22 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}--}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{x{2.56 cm} x{5.44 cm} }
\SetRowColor{DarkBackground}
\mymulticolumn{2}{x{8.4cm}}{\bf\textcolor{white}{Other Commands}}  \tn
% Row 0
\SetRowColor{LightBackground}
`TAB` & Indent current line, cycles between points \tn 
% Row Count 2 (+ 2)
% Row 1
\SetRowColor{white}
`S-TAB` & Indent current line, cycles in opposite direction \tn 
% Row Count 4 (+ 2)
% Row 2
\SetRowColor{LightBackground}
`M-.` & Go to definition of identifier under point \tn 
% Row Count 6 (+ 2)
% Row 3
\SetRowColor{white}
Middle mouse button & Go to definition of identifier clicked on \tn 
% Row Count 8 (+ 2)
% Row 4
\SetRowColor{LightBackground}
`M-*` & Go back (Emacs \textless{} 25.1) \tn 
% Row Count 9 (+ 1)
% Row 5
\SetRowColor{white}
`M-,` & Go back (Emacs \textgreater{}= 25.1) \tn 
% Row Count 10 (+ 1)
\hhline{>{\arrayrulecolor{DarkBackground}}--}
\end{tabularx}
\par\addvspace{1.3em}


% That's all folks
\end{multicols*}

\end{document}