Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unofficial fix to the LaTeX generation of Code...

Email Gateway (Dec 03 2025 at 10:34):

From: Winston Ren <cl-isabelle-users@lists.cam.ac.uk>

Dear all,

I have an unofficial fix to the Code2HTML plugin in Isabelle. I noticed the plugin was not working properly with LaTeX generation due to out-of-date packages used and repeated object constructors. So I made some fixes:

1.
Used package xcolor instead of color.
2.
Abandoned the old package \\usepackage[latin1]{inputenc} for encoding special characters from Isabelle; instead, used a combination of \\setmainfont{Latin Modern Roman}, \\setmathfont{Latin Modern Math}, and \\setmonofont{JetBrains Mono} to display special characters. Accordingly, the compiler uses XeLaTeX instead of pdfLaTeX.
3.
Fixed the indentation problem from the old version.
4.
In GenericDocument.Java there was a repeated call to the style constructors, resulting in a repeated style definition export in the LaTeX script generated. This was fixed by adding a style detection method.

The full source code can be found in the following GitHub repo, with a compiled working JAR file.
GitHub Repository: https://github.com/FullBackward/Code2HTML-Isabelle-version-
Please let me know if you find this fix useful or if you find any remaining problems.

Winston Ren

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th' ann an Oilthigh Dh?n ?ideann, cl?raichte an Alba, ?ireamh cl?raidh SC005336.

Email Gateway (Dec 03 2025 at 12:17):

From: Makarius <makarius@sketis.net>

On 03/12/2025 11:23, Winston Ren (via cl-isabelle-users Mailing List) wrote:

The full source code can be found in the following GitHub repo, with a
compiled working JAR file.
GitHub Repository: https://github.com/FullBackward/Code2HTML-Isabelle-version-
<https://github.com/FullBackward/Code2HTML-Isabelle-version->
Please let me know if you find this fix useful or if you find any remaining
problems.

You can make this official by contacting the jEdit project
https://www.jedit.org and submit patches there. The jEdit guys might
eventually hand over the responsibility for the Code2HTML to you.

Further note that starting with Isabelle2025-1 (December 2025), the bundled
version of jEdit no longer includes Code2HTML.jar (and Navigator.jar), so you
can use the normal jEdit plugin management without special considerations.

The current approximation of the coming release is
https://isabelle.in.tum.de/website-Isabelle2025-1-RC3

Makarius

Last updated: Dec 21 2025 at 20:24 UTC