[isabelle] document preparation: folding inside ignored parts



Hi,

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"
  by simp
  (*>*)

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.

Cheers,

Bertram

P.S. I started with ROOT and root.tex as generated by isabell mkroot -d,
and then modified the ROOT file as follows:

session "doctest" = "HOL" +
  options [document = pdf, document_output = "output", document_variants="document:outline=/proof,/ML"]
  theories
    Scratch
  document_files
    "root.tex"




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