waynee95 (Nov 07 2021 at 13:43): waynee95 (Nov 07 2021 at 13:43):How can I enable printing double quotes when generating pdf output from Isabelle theories?
I want the code in the pdf to look the same as in the original source, so I don't want the double quotes to be removed.
Mathias Fleury (Nov 07 2021 at 13:47):Quotes are not removed from the HTML output and the code is identitcal with some syntax highlighting (e.g., http://people.mpi-inf.mpg.de/~mfleury/IsaFoL/current/Weidenbach_Book/CDCL/DPLL_W.html)
Mathias Fleury (Nov 07 2021 at 13:54):LaTeX at the very least will add linebreaks
waynee95 (Nov 07 2021 at 14:14):But I don't want to generate HTML, I want to build a pdf.
When I have the this code in Isabelle:
fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 m = m" |
"add (Suc n ) m = Suc (add n m)"
lemma "add m 0 = m"
apply (induction m)
apply (auto)
done
and then use isabelle build to build a document.pdf, that pdf will have all double quotes removed but I want them to not be removed. Is this possible?
Mathias Fleury (Nov 07 2021 at 14:23):If I understand the prelude.tex of the prog-prove (~~src/Doc/Prog_Prove/document/prelude.tex), this should do the job:
\chardef\isachardoublequote=`\"%
\chardef\isachardoublequoteopen=`\"%
\chardef\isachardoublequoteclose=`\"%
\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
\renewcommand{\isacharbackquoteclose}{\isacharbackquote}
I am so used to ignoring the quotes that I find it weird to see them in any place that is not a tutorial...
Last updated: Jul 15 2022 at 23:21 UTC