[isabelle-dev] isabelle build for generating TeX Snippets

[Christian Sternagel]

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
>