Email Gateway (Aug 22 2022 at 16:35): Email Gateway (Aug 22 2022 at 16:35):From: Lars Hupel <hupel@in.tum.de>
Dear list,
as some of you might be aware, the "\bf", "\it" etc. commands have been
deprecated in LaTeX for over two decades.
Document classes like "article" still define them as follows:
<https://tex.stackexchange.com/a/346876>.
However, other document classes, like the popular KOMA-Script package,
have stopped doing so. This means that Isabelle-produced LaTeX documents
fail to compile with that document class (they used to compile at some
point in the past).
The reason appears to be that "isabelle.sty" still uses these ancient
commands, e.g. here:
\newcommand{\isakeyword}[1]
{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
... in what appears to be a mixture between old- and new-style.
I would like to advocate for replacing all ancient commands by their
newer counterparts.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:35):From: Makarius <makarius@sketis.net>
Here is a related thread:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-May/msg00008.html
What is actually your proposal?
I would have used \textbf{}, but it might be wrong. The precise
semantics of LaTeX font style commands is still somewhat unclear to me
after so many decades -- and the KOMA guy is doing strange things after all.
Makarius
Email Gateway (Aug 22 2022 at 16:35):From: Lars Hupel <hupel@in.tum.de>
Here is a related thread:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-May/msg00008.html
Ah, I forgot all about that one. But it doesn't look like anything
useful came out of there, except for the well-known workaround.
What is actually your proposal?
Remove all occurrences of macros that have been deprecated for over two
decades from "isabelle.sty".
I would have used \textbf{}, but it might be wrong. The precise
semantics of LaTeX font style commands is still somewhat unclear to me
after so many decades -- and the KOMA guy is doing strange things after all.
I don't think so. KOMA-Script is an island of reasonableness in an
otherwise unstructured world, mostly because of its sensible defaults.
In any case, I don't think Isabelle should produce LaTeX output that
can't be compiled with one of the most popular document classes out there.
Email Gateway (Aug 22 2022 at 16:35):From: Makarius <makarius@sketis.net>
The typesetting in the Isabelle style files cannot be changed, without
destroying an unknown number of existing documents.
The precise definitions for these LaTeX 2.09 macros are as follows (from
article.cls):
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
Resetting to \normalfont was a well-known "feature" of LaTeX before 2e
came out (as approximation for the planned LaTeX 3). That fine-point is
actually required in the Isabelle style files: often there is a
surrounding \emph{} for italic correction, but the intended font style
is set later: italics needs to be reset. (I devised that trick in 1999.
Before it was infeasible to have text and quasi-math side-by-side,
without knowing its structure as a TeX formula. Maybe there are better
ways today.)
In Isabelle/a93a9e89da72, I have now expanded the above macros
faithfully according to the definitions (for text mode), but this is
only for the next Isabelle release in > 6 months.
Hopefully nobody copies around variant versions of isabelle.sty files:
such clones become outdated rather quickly, and sometimes even end up in
the AFP repository.
As intermediate solution for official Isabelle releases it is better to
put definitions for \rm etc. into the root.tex.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC