[isabelle-dev] isabelle build for generating TeX Snippets

[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