Changed behaviour of (*<*) ... (*>*)

[Achim D. Brucker]

Hi,
I did some bisection. The changset that introduced the new behaviour is 
"85275:e50cdc94cf5d".

Starting with this changeset, text enclosed in (*<*) ... (*>*) is no 
longer excluded from the LaTeX/PDF generation. I assume this results in 
a "silent" change for most applications (i.e., some text is now included 
in the PDF that was not intended to be excluded). For one of the AFP 
entries (Isabelle_DOF) I co-authored, this is resulting in a hard 
compilation error, as some invalid LateX code is intentionally excluded 
from the final LaTeX/PDF generation using (*<*) ... (*>*).

Best,
Achim

On 27/08/2026 10:32, Achim D. Brucker wrote:
> 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
>
>
]