From: Francesco Mazzoli Date: Sat, 15 Jun 2013 10:48:12 +0000 (+0100) Subject: add agda.sty, to be safe X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=cf00b161aba79b600a069d07870a076303f79de8 add agda.sty, to be safe --- diff --git a/agda.sty b/agda.sty new file mode 100644 index 0000000..850cd05 --- /dev/null +++ b/agda.sty @@ -0,0 +1,242 @@ +% ---------------------------------------------------------------------- +% Some useful commands when doing highlighting of Agda code in LaTeX. +% ---------------------------------------------------------------------- + +\ProvidesPackage{agda} + +\usepackage{ifxetex, xcolor, polytable, ifthen} + +% XeLaTeX +\ifxetex + \usepackage{polyglossia} + \usepackage{fontspec} + \usepackage[]{unicode-math} + +% pdfLaTeX +\else + \usepackage{ucs, amsfonts, amssymb} + \usepackage[safe]{tipa} % See page 12 of the tipa manual for what + % safe does. + + % FIX: This doesn't seem to help solve the pipe problem? + % http://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex + \usepackage[T1]{fontenc} + \usepackage[utf8x]{inputenc} + + % FIX: Complete the list and send it upstream to the ucs package devs. + \DeclareUnicodeCharacter{9657}{$\triangleright$} + \DeclareUnicodeCharacter{8759}{::} + \DeclareUnicodeCharacter{8263}{$?\!?$} + \DeclareUnicodeCharacter{737} {$^l$} % FIX: Ugly, apparently ^r is + % defined, I can't find the + % definition though. + \DeclareUnicodeCharacter{8718}{$\blacksquare$} + \DeclareUnicodeCharacter{8255}{$\_$} % FIX: Couldn't find \undertie. + \DeclareUnicodeCharacter{9667}{$\triangleleft$} + \DeclareUnicodeCharacter{10218}{$\langle\!\langle$} + \DeclareUnicodeCharacter{10219}{$\rangle\!\rangle$} +\fi + +% ---------------------------------------------------------------------- +% Colour schemes. + +\newcommand{\AgdaColourScheme}{standard} + +\DeclareOption{bw} {\renewcommand{\AgdaColourScheme}{bw}} +\DeclareOption{conor}{\renewcommand{\AgdaColourScheme}{conor}} +\ProcessOptions\relax + +% ---------------------------------------------------------------------- +% Font styles. + +% Default font style. +\newcommand{\AgdaFontStyle}[1]{\textsf{#1}} + +% Keyword font style. +\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ + \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}} +}{ + \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}} +} + +% String font style. +\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}} + +% Comment font style. +\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}} + +% Bounded variables font style. +\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}} + +% ---------------------------------------------------------------------- +% Colours. + +% ---------------------------------- +% The black and white colour scheme. +\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ + + % Aspect colours. + \definecolor{AgdaComment} {HTML}{000000} + \definecolor{AgdaKeyword} {HTML}{000000} + \definecolor{AgdaString} {HTML}{000000} + \definecolor{AgdaNumber} {HTML}{000000} + \definecolor{AgdaSymbol} {HTML}{000000} + \definecolor{AgdaPrimitiveType}{HTML}{000000} + \definecolor{AgdaOperator} {HTML}{000000} + + % NameKind colours. + \definecolor{AgdaBound} {HTML}{000000} + \definecolor{AgdaInductiveConstructor} {HTML}{000000} + \definecolor{AgdaCoinductiveConstructor}{HTML}{000000} + \definecolor{AgdaDatatype} {HTML}{000000} + \definecolor{AgdaField} {HTML}{000000} + \definecolor{AgdaFunction} {HTML}{000000} + \definecolor{AgdaModule} {HTML}{000000} + \definecolor{AgdaPostulate} {HTML}{000000} + \definecolor{AgdaPrimitive} {HTML}{000000} + \definecolor{AgdaRecord} {HTML}{000000} + + % Other aspect colours. + \definecolor{AgdaDottedPattern} {HTML}{000000} + \definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3} + \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE} + \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3} + \definecolor{AgdaError} {HTML}{696969} + + % Misc. + \definecolor{AgdaHole} {HTML}{BEBEBE} + +% ---------------------------------- +% Conor McBride's colour scheme. +}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{ + + % Aspect colours. + \definecolor{AgdaComment} {HTML}{B22222} + \definecolor{AgdaKeyword} {HTML}{000000} + \definecolor{AgdaString} {HTML}{000000} + \definecolor{AgdaNumber} {HTML}{000000} + \definecolor{AgdaSymbol} {HTML}{000000} + \definecolor{AgdaPrimitiveType}{HTML}{0000CD} + \definecolor{AgdaOperator} {HTML}{000000} + + % NameKind colours. + \definecolor{AgdaBound} {HTML}{A020F0} + \definecolor{AgdaInductiveConstructor} {HTML}{8B0000} + \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000} + \definecolor{AgdaDatatype} {HTML}{0000CD} + \definecolor{AgdaField} {HTML}{8B0000} + \definecolor{AgdaFunction} {HTML}{006400} + \definecolor{AgdaModule} {HTML}{006400} + \definecolor{AgdaPostulate} {HTML}{006400} + \definecolor{AgdaPrimitive} {HTML}{006400} + \definecolor{AgdaRecord} {HTML}{0000CD} + + % Other aspect colours. + \definecolor{AgdaDottedPattern} {HTML}{000000} + \definecolor{AgdaUnsolvedMeta} {HTML}{FFD700} + \definecolor{AgdaTerminationProblem}{HTML}{FF0000} + \definecolor{AgdaIncompletePattern} {HTML}{A020F0} + \definecolor{AgdaError} {HTML}{F4A460} + + % Misc. + \definecolor{AgdaHole} {HTML}{9DFF9D} + +% ---------------------------------- +% The standard colour scheme. +}{ + % Aspect colours. + \definecolor{AgdaComment} {HTML}{B22222} + \definecolor{AgdaKeyword} {HTML}{CD6600} + \definecolor{AgdaString} {HTML}{B22222} + \definecolor{AgdaNumber} {HTML}{A020F0} + \definecolor{AgdaSymbol} {HTML}{404040} + \definecolor{AgdaPrimitiveType}{HTML}{0000CD} + \definecolor{AgdaOperator} {HTML}{000000} + + % NameKind colours. + \definecolor{AgdaBound} {HTML}{000000} + \definecolor{AgdaInductiveConstructor} {HTML}{008B00} + \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500} + \definecolor{AgdaDatatype} {HTML}{0000CD} + \definecolor{AgdaField} {HTML}{EE1289} + \definecolor{AgdaFunction} {HTML}{0000CD} + \definecolor{AgdaModule} {HTML}{A020F0} + \definecolor{AgdaPostulate} {HTML}{0000CD} + \definecolor{AgdaPrimitive} {HTML}{0000CD} + \definecolor{AgdaRecord} {HTML}{0000CD} + + % Other aspect colours. + \definecolor{AgdaDottedPattern} {HTML}{000000} + \definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00} + \definecolor{AgdaTerminationProblem}{HTML}{FFA07A} + \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3} + \definecolor{AgdaError} {HTML}{FF0000} + + % Misc. + \definecolor{AgdaHole} {HTML}{9DFF9D} +}} + +% ---------------------------------------------------------------------- +% Commands. + +% Aspect commands. +\newcommand{\AgdaComment} [1] + {\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}} +\newcommand{\AgdaKeyword} [1] + {\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}} +\newcommand{\AgdaString} [1]{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}} +\newcommand{\AgdaNumber} [1]{\textcolor{AgdaNumber}{#1}} +\newcommand{\AgdaSymbol} [1]{\textcolor{AgdaSymbol}{#1}} +\newcommand{\AgdaPrimitiveType}[1] + {\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}} +\newcommand{\AgdaOperator} [1]{\textcolor{AgdaOperator}{#1}} + +% NameKind commands. +\newcommand{\AgdaBound} [1]{\AgdaBoundFontStyle{\textcolor{AgdaBound}{#1}}} +\newcommand{\AgdaInductiveConstructor}[1] + {\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{#1}}} +\newcommand{\AgdaCoinductiveConstructor}[1] + {\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{#1}}} +\newcommand{\AgdaDatatype} [1]{\AgdaFontStyle{\textcolor{AgdaDatatype}{#1}}} +\newcommand{\AgdaField} [1]{\AgdaFontStyle{\textcolor{AgdaField}{#1}}} +\newcommand{\AgdaFunction} [1]{\AgdaFontStyle{\textcolor{AgdaFunction}{#1}}} +\newcommand{\AgdaModule} [1]{\AgdaFontStyle{\textcolor{AgdaModule}{#1}}} +\newcommand{\AgdaPostulate}[1]{\AgdaFontStyle{\textcolor{AgdaPostulate}{#1}}} +\newcommand{\AgdaPrimitive}[1]{\AgdaFontStyle{\textcolor{AgdaPrimitive}{#1}}} +\newcommand{\AgdaRecord} [1]{\AgdaFontStyle{\textcolor{AgdaRecord}{#1}}} + +% Other aspect commands. +\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}} +\newcommand{\AgdaUnsolvedMeta} [1] + {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}} +\newcommand{\AgdaTerminationProblem}[1] + {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}} +\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}} +\newcommand{\AgdaError} [1] + {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}} + +% Misc. +\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}} +\long\def\AgdaHide#1{} % Used to hide code from LaTeX. + +\newcommand{\AgdaIndent}[1]{\quad} + +% ---------------------------------------------------------------------- +% The code environment. + +\newcommand{\AgdaCodeStyle}{} +% \newcommand{\AgdaCodeStyle}{\tiny} + +\ifdefined\mathindent + {} +\else + \newdimen\mathindent\mathindent\leftmargini +\fi + +\newenvironment{code}% +{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed}% +{\endpboxed\par\noindent% +\ignorespacesafterend} + +% Default column for polytable. +\defaultcolumn{l}