Max Nowak (May 27 2021 at 13:27): Max Nowak (May 27 2021 at 13:27):I'm writing a larger document in LaTeX, and while it is primarily in classic math notation, I want to include some interesting Isabelle/HOL snippets. So far (i.e. not very far yet :D) I've used verbatim, but verbatim has issues with ∀, ⇒, etc. I am aware of https://isabelle.in.tum.de/doc/sugar.pdf, however I do not want to typeset my whole document in Isabelle, merely a few snippets, which doesn't have to be 1:1 what isabelle sugar would produce.
I also found https://github.com/lammich/isabelle_llvm/blob/master/papers/2021_Enschede_Talk/lstisabelle.tex which looks promising but has rough edges and depends on some auto-generated isabelle tex files which give me plenty of LaTeX errors.
Is there some easy-to-use style I can just import and get pretty isabelle listings?
Max Nowak (May 27 2021 at 13:31):Main concerns are rendering unicode symbols (forall, etc) in the listings, maybe bold and/or colored keywords.
Lukas Stevens (May 27 2021 at 13:35):I just use
\usepackage{listings}
\definecolor{isarblue}{HTML}{006699}
\definecolor{isargreen}{HTML}{009966}
\lstdefinelanguage{isabelle}{%
keywords=[1]{type_synonym,datatype,fun,abbreviation,definition,proof,lemma,theorem,corollary},
keywordstyle=[1]\bfseries\color{isarblue},
keywords=[2]{where,assumes,shows,and},
keywordstyle=[2]\bfseries\color{isargreen},
keywords=[3]{if,then,else,case,of,SOME,let,in,O},
keywordstyle=[3]\color{isarblue},
}
\lstset{%
language=isabelle,
escapeinside={&}{&},
columns=fixed,
extendedchars,
basewidth={0.5em,0.45em},
basicstyle=\ttfamily,
mathescape,
}
Unicode symbols go inside mathescape $.
Lukas Stevens (May 27 2021 at 13:35):You might need to fiddle around to get it typeset in a nice way though.
Last updated: Apr 26 2024 at 04:17 UTC