search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

tex generation: avoid '\rm', load mathtools and phonetic #130

Closed benjub closed 1 year ago

benjub commented 1 year ago

There remain some \tt that should be replaced by either texttt{ or \mathtt{ depending on whether we are in text or math mode (was not obvious at first in the C code).

Also, I added the phonetic package, so that we can replace the latexdef's using \rotate with \riota, and then one can remove the graphicx package.

benjub commented 1 year ago

Is it good for you @digama0 ?

benjub commented 1 year ago

Looks good to you @digama0 ?

The package mathrsfs that I add in this PR is necessary for the LaTeX files generated by metamath.c to compile. I added the package mathtools for better spacing and the package phonetic to be able to typeset riota more simply. Finally, I removed the occurrences of the deprecated \rm. I did not remove the deprecated \tt since I could not be sure they appear in math mode (in which case they should be \mathtt) or text mode (hence \texttt).

digama0 commented 1 year ago

Can you move the style changes to a separate PR?

benjub commented 1 year ago

Can you move the style changes to a separate PR?

Done in #131 (well, the non-style part is #131).