Email Gateway (Aug 22 2022 at 10:19): Email Gateway (Aug 22 2022 at 10:19):From: Makarius <makarius@sketis.net>
(This thread still looks unresolved, although the deadline might already
have passed.)
Isabelle document preparation is merely a certain schematic way to
generate LaTeX macros. The meaning is defined by the LaTeX styles and
other setup. The defaults work for the most common document classes, but
nothing is for sure in LaTeX.
Included is the result of experimenting with sig-alternate.cls for 30min.
It looks fine so far, compared to the standard example document for that
style.
The main Isabelle macro setup is something like this:
\isabellestyle{it}
\renewcommand{\isastyletext}{\normalfont\normalsize}
\renewcommand{\isastyletxt}{\normalfont}
\renewcommand{\isastylecmt}{\normalfont}
Sometimes it is also necessary to redefine sectioning macros
\isamarkupsection{} etc. The basic assumption is that the underlying
\section{} resets all font styles as required, but this is not always the
case.
Makarius
Test_SIG_Alternate.tar.gz
Email Gateway (Aug 22 2022 at 10:19):From: Toby Murray <toby.murray@nicta.com.au>
Thank you Makarius for taking the time to look at this, and for
providing a solution, and giving the info I'd need to sort this out on
my own next time.
Thanks again
Toby
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:22):From: Toby Murray <toby.murray@nicta.com.au>
Hi all,
There appears to be a long-standing issue with sig-alternate.cls and
Isabelle document preparation, dating back to at least 2004 [1], that is
currently biting me.
Specifically, \isabellestyle{it} causes paragraph text to be rendered in
italics when using sig-alternate.cls as the document class.
It looks like this has hit others in the past [2], where the solution
there seemed to be to avoid \isabellestyle{it} altogether and use
\isabellestyle{rm} instead [3].
Is there a standard workaround I can employ to have italic typeset maths
when using sig-alternate.cls ?
Thanks
Toby
[1] https://groups.google.com/forum/#!topic/fa.isabelle/x2CL8uKbcOM
[2]
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/nominal2/raw-diff/e96f3efb0032/Quotient-Paper/document/root-sac.tex
[3]
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/nominal2/raw-annotate/d769c24094cf/Quotient-Paper/document/root.tex
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:28):From: Buday Gergely <gbuday@karolyrobert.hu>
Dear Toby,
my solution was, tripped from comments:
\documentclass{sig-alternate}
\pdfpagewidth=8.5truein
\pdfpageheight=11truein
\usepackage{isabelle,isabellesym}
\usepackage[utf8]{inputenc}
\usepackage{pdfsetup}
\urlstyle{rm}
\newcommand{\isabellestyleup}{%
\def\isastyle{\normalfont\small}%
\def\isastyleminor{\normalfont\small}%
\def\isastylescript{\normalfont\footnotesize}%
\isachardefaults%
}
\isabellestyle{up}
\begin{document}
...
I hope this helps.
Email Gateway (Aug 22 2022 at 10:34):From: Toby Murray <toby.murray@nicta.com.au>
Thanks, Buday. This seems to give reliable typesetting of formulas in
roman.
I'll keep this as a backup option if I can't manage to work out how to
get italics.
Toby
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 18 2024 at 08:19 UTC