Email Gateway (Nov 30 2020 at 14:24): Email Gateway (Nov 30 2020 at 14:24):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Hi again.
My team is formalizing mathematics that is most naturally written using
subscripts and superscripts. By using the patch in
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-August/msg00055.html
we've been able to make them look very nicely in jEdit. But the PDF
rendering of sub/superscripts looks a bit odd because the font doesn't
seem to scale appropriately.
This seem to stem from the use of "\mbox" in the definition of
\isactrlbsub, \isactrlesub, \isactrlbsup and \isactrlesup.
Is this the normal behavior? Or there is some customization I'm missing?
I experimented with an alternative definition that seems to work, using
the package "relsize". It requires adding
\RequirePackage{relsize}
to the isabelle.sty style file and replacing "\isastylescript" by
"\itshape\smaller" in the above macros' definitions:
\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\itshape\smaller}
\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\itshape\smaller}
\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
This gives the following output:
Thanks in advance,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
giaojfdcgocffblm.png
fmaclclgnfhpimhp.png
Email Gateway (Dec 01 2020 at 22:29):From: "David E. Narvaez" <den9562@rit.edu>
My apologies for hijacking your thread with a tangentially related question. I
understand the issues in this and the linked thread are regarding arguments as
(sub|super)scripts. Nevertheless, in my case I want (sub|super)scripts just
for pretty-printing in jEdit. What is the syntax for that? I for now tried
prepending every character I wanted as a subscript with ⇩ and it works (e.g.
Z⇩m⇩o⇩d), but I wonder if there is a proper way to display multicharacter
subscripts. \<bsup>/\<esup> did not work.
I am working with Isabelle 2020 for what is worth. Thanks in advance for any
help you can provide.
Email Gateway (Dec 01 2020 at 22:36):From: Makarius <makarius@sketis.net>
Yes, this is the proper way. There is some support for it Isabelle/jEdit: mark
a selection and use the normal actions isabelle.control-sub /
isabelle.control-sup (see also the "jedit" Documentation).
Makarius
Email Gateway (Dec 02 2020 at 18:49):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 1/12/20 a las 19:28, David E. Narvaez escribió:
That was the point of my original query at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00089.html
The only way to make the patch work is to get a copy of the Isabelle
repository, apply the patch, and rebuild.
I don't recall if there was further discussion on the possibility of
making this part of Isabelle, but I'd be glad to know why it is not the
case.
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Last updated: Jan 04 2025 at 20:18 UTC
