Stream: Beginner Questions

Topic: ✔ Double quotes in pdf output


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mathias Fleury (Nov 07 2021 at 13:54):

LaTeX at the very least will add linebreaks

view this post on Zulip 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?

view this post on Zulip 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}

view this post on Zulip Mathias Fleury (Nov 07 2021 at 14:25):

I am so used to ignoring the quotes that I find it weird to see them in any place that is not a tutorial...

view this post on Zulip waynee95 (Nov 07 2021 at 18:03):

Ah thanks! That does the trick. I have been skimming the prog-prove source but I didn't look close enough then.
I only want to show double quotes because I am prepping course material.

view this post on Zulip Notification Bot (Nov 07 2021 at 18:04):

waynee95 has marked this topic as resolved.


Last updated: Aug 15 2022 at 02:13 UTC