Re: [isabelle] document preparation: folding inside ignored parts
On Sat, 27 Jun 2015, Bertram Felgenhauer via Cl-isabelle-users wrote:
I've encountered an oddity in Isabelle's (2015) document preparation.
I have a theory with some boring facts that I want to hide from the
generated documents, so I'm using (*<*)/(*>*) like this:
lemma some_boring_lemma: "1+2 = 3"
This works as expected (no output is produced for this lemma nor its
proof) by default. But if proofs are folded (e.g. using the recipe for
outlines from the tutorial), then the folded proof appears in the
generated outline, despite belonging to the ignored material.
This is a conflict of features: the older (*<*)(*>*) pseudo-comments (from
2000) don't work together with the newer concept of "tags" (from 2005);
note that a proof has such a default %"proof" tag and can thus be folded.
You can try to use just the tag concept alone, notably with annotations
lemma %invisible boring
There are slightly different rules for whitespace handling, but that is a
black art in any case.
This archive was generated by a fusion of
Pipermail (Mailman edition) and