(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
