[isabelle-dev] isabelle build for generating TeX Snippets
c-sterna at jaist.ac.jp
Tue Nov 6 06:04:14 CET 2012
(I send this message to the development list since isabelle build is not
yet part of any official release.)
How could we translate the instructions from
for use with "isabelle build"?
More specifically, I currently have the ROOT file
session "Snippets" = "HOL" +
document = "pdf",
document_output = "generated",
document_variants = "snippets",
show_question_marks = "false"]
and the document/build file:
"$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)?
More information about the isabelle-dev