[isabelle-dev] isabelle build for generating TeX Snippets

[Gerwin Klein]

The approach in LaTeX Sugar is very similar, but I don't remember if we describe there how to avoid generating the superfluous pdf.

You can basically use a script document/build that takes over control of which commands are run to build the document. That command could for instance just be "touch document.pdf" if you don't want to build anything at all in that run.

Some example build scripts are in src/Doc/*/document/

Cheers,
Gerwin

On 06/11/2012, at 9:48 PM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote:

> Thanks! I will have a look at LaTeX Sugar then. Just for clarification: My application are TeX snippets that are not generated from antiquotations (namely parts of Isar proofs). However, I use almost the same approach as described in the wiki, the only difference being that I have to surround the parts that I want to have in a snipped by text_raw or txt_raw, rather than plain text or txt (since I split the begin and the end of a LaTeX environment).
> 
> cheers
> 
> chris
> 
> On 11/06/2012 06:44 PM, Tobias Nipkow wrote:
>> 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
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>