Changed behaviour of (*<*) ... (*>*)
Achim D. Brucker
adbrucker at 0x5f.org
Thu Aug 27 11:32:04 CEST 2026
Hi,
While trying to address a build failure of one of our AFP entries, I
spottedĀ (*<*) ... (*>*) does not seem to exclude parts from being
included in the generated LaTeX/PDF document. For instance, generating a
PDF from the the theory
theory Ex imports Main begin
(*<*)text\<open>Should this be included in the generated PDF?\<close>(*>*)
end
does not include the text "Should this be included in the generated
PDF?" in the generated PDF when using Isabelle 2025-2 but is included
when using the latest version from the repository (TIP:
85327:dc45b445012a).
By quickly skimming over the NEWS entries an the hg log messages, I
could not find out whether this is intentional or not.
I would appreciate any advise on how I should upgrade my theories to
make them ready for the future.
Thanks a lot!
Best,
Achim
More information about the isabelle-dev
mailing list