[isabelle-dev] isabelle build for generating TeX Snippets

[Tobias Nipkow]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev