Email Gateway (Aug 22 2022 at 13:42): Email Gateway (Aug 22 2022 at 13:42):From: Gergely Buday <gbuday@karolyrobert.hu>
Hi,
I would like to generate PDFs through the document preparation system
in a way that I would see the original Isar sources with the font Isabelle/jEdit uses on the screen.
Including outer syntax, so quoting marks included.
The usual pipeline discards these.
Is there a solution that would not use antiquotations? I would like not to repeat the code if possible.
I guess this is outside the document preparation system, but this is what I would really want, in a pdf:
http://isabelle.in.tum.de/library/HOL/HOL/Code_Generator.html
Is this doable?
Email Gateway (Aug 22 2022 at 13:42):From: Gergely Buday <gbuday@karolyrobert.hu>
I have found something in the System manual on page 22:
https://isabelle.in.tum.de/dist/Isabelle2016/doc/system.pdf#page=25
so I tried
isabelle build -o browser_info -o document=pdf -v -c isartutorial
for that I got
*** Undefined session(s): "isartutorial"
where I used the session name in the ROOT file.
The examples in the System manual used library names, is this feature available only for them?
How can I define the session name for this?
Email Gateway (Aug 22 2022 at 13:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Gergely,
Is your ROOT file registered in any of the ROOTS files of the distribution? If not, you
have to add the path to ROOT's folder to the search path using the option -d.
isabelle build -d <path_to_ROOT_folder> -o browser_info -o document=pdf -v -c <session>
-o browser_info generates the HTML output similar to your example.
-o document=pdf generates the LaTeX documents, but they do not look like the HTML versions.
Hope this helps,
Andreas
Last updated: Apr 23 2024 at 08:19 UTC