On 27/09/2020 21:26, Makarius wrote:
>
> This refers to Isabelle/684f14b1e7fc (and AFP/35158287da0b).
>
> At the Isabelle Workshop 2020, Clemens Ballarin proposed to switch to LuaLaTeX
> by default: it allows advanced packages programmed in the Lua scripting
> language.
One more thing: using visual diffpdf on Ubuntu 18.04, I have compared various
important "doc" entries, e.g. prog-prove, jedit, implementation, isar-ref.
After Isabelle/8162ca81ea8a the results are mostly identical, with a few minor
deviations in font-metrics and hyphenation: both work generally better in
LuaLaTeX.
There might be more fine points to watch out for.
As a general principle, documents that use Isabelle mechanisms like the
@{verbatim} or @{text} antiquotations work better than low-level
"LaTeX-drawings" done manually (e.g. \verbatim and $...$).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
