Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sub/superscripts in document preparation


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC