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