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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
