[isabelle-dev] isabelle build for generating TeX Snippets
nipkow at in.tum.de
Tue Nov 6 10:44:10 CET 2012
I think we stumbled across the same problem (unless I am mistaken, in which case
Gerwin can tell you how we solved it).
This does not solve your problem but may still be of interest: In the
development version of the LaTeX Sugar manual, there is a description how to
create tex snippets of Isabelle theory files. This is relevant for text that you
cannot generate by antiquotations or that you want to format in a specific manner.
Am 06/11/2012 06:04, schrieb Christian Sternagel:
> (I send this message to the development list since isabelle build is not yet
> part of any official release.)
> Dear all,
> How could we translate the instructions from
> for use with "isabelle build"?
> More specifically, I currently have the ROOT file
> session "Snippets" = "HOL" +
> options [
> document = "pdf",
> document_output = "generated",
> document_variants = "snippets",
> show_question_marks = "false"]
> and the document/build file:
> set -e
> "$ISABELLE_TOOL" latex -o "$FORMAT"
> sed -n '/DefineSnippet/,/EndSnippet/p' Snippets.tex > ../snippets.tex
> together with a theory file Snippets.thy that contains the actual snippets. What
> is a bit annoying about this setup, is that I actually have to build a file
> snippets.pdf (hence also the otherwise irrelevant files document/root.tex,
> document/isabelle.sty, and document/isabellesym.sty) just to obtain the file
> generated/snippets.tex. Any suggestions how to do this directly (without falling
> back to an IsaMakefile)?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev