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

[Makarius]

On 05/09/2026 20:55, Achim D. Brucker wrote:
> 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 
> (*<*) ... (*>*).

Hi Achim,

there is definitely something wrong in my side, but I did not find time yet to 
figure out the details. Presently, the next defined snapshot will be 
Isabelle2026-RC1. In between, many things can be wrong in many ways.


	Makarius