Re: [isabelle] Common options in ROOT

On Thu, 7 Feb 2013, Joachim Breitner wrote:

I’m currently writing a ROOT file for a set of exercise sheets that uses
the tags feature to generate both a variant without solutions and a
variant with solutions from the same file. Currently, the file looks
like this:

       session Uebung1 = HOL +
       	options [document=pdf, document_variants="document=+template,-templateoops,/solution:solution=-template,-templateoops,+solution"]
       	theories "Deduction"
       	files "document/root.tex"

       session Uebung2 = HOL +
       	options [document=pdf, document_variants="document=+template,-templateoops,-onlysolution,/solution:solution=-template,-templateoops,+onlysolution,+solution"]
       	theories "Simplification"
       	files "document/root.tex"

Can I somehow set these options for all sessions in the file, or define a “base session” that does not add any theory and just sets options?

I tried to make sessions as declarative and self-contained as feasible, so there is no way for common options, apart from global ISABELLE_BUILD_OPTIONS or similar. But document_variants should indeed be associated with the document session in question.

What you can do is to delegate interpretation of document variants to the document job. You merely specify names in ROOT and re-adjust the latex environments for tags later. You can do completely different things, of course. In Isabelle2013 document variants are more flexibile than before.

Included is an example for Isabelle2013-RC1/RC2/RC3. ROOT merely specifies document_variants="foo:bar" and root_foo.tex, root_bar.tex determine what happens.

Just after making the Isabelle2013-RC3 snapshot, I realized that "isabelle document" needs a tiny repair as in the included "ch" changeset.


Attachment: Variants.tar.gz
Description: GNU Zip compressed data

# HG changeset patch
# User wenzelm
# Date 1360239605 -3600
# Node ID 70a4c11cd79eecec7cf08bdee862b75935527975
# Parent  bece235e305408ba2435058f8dea50e7a7f49398
proper root for document variants (cf. be8002ee43d8);

diff -r bece235e3054 -r 70a4c11cd79e lib/Tools/document
--- a/lib/Tools/document	Thu Feb 07 12:08:37 2013 +0100
+++ b/lib/Tools/document	Thu Feb 07 13:20:05 2013 +0100
@@ -124,7 +124,7 @@
   "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" && \
   { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
   { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
-  "$ISABELLE_TOOL" latex -o "$FMT"
+  "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex"

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.