Hi Christian, 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. Tobias 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 > > https://isabelle.in.tum.de/community/Generate_TeX_Snippets > > 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"] > theories > Snippets > files > "document/build" > "document/root.tex" > "document/isabelle.sty" > "document/isabellesym.sty" > > and the document/build file: > > #!/bin/bash > > set -e > > FORMAT="$1" > VARIANT="$2" > > "$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)? > > cheers > > chris > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
