Email Gateway (Aug 22 2022 at 14:27): Email Gateway (Aug 22 2022 at 14:27):From: Tobias Nipkow <nipkow@in.tum.de>
Question: how does Isabelle estimate the size of the latex output if the string
contains \<^latex>\<open>xxx\<close> blocks? In the past (\<^raw>) I had the
idea that they don't count at all, but I don't know where I got that impression
from. Empirically they do seem to be counted - maybe roughly the length of xxx?
Thanks
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:28):From: Makarius <makarius@sketis.net>
The old \<^raw> encoding did indeed count the length as 0, because any
control symbol is supposed to be non-printable.
I have now imitated that for \<^latex>\<open>xxx\<close> as well in
https://bitbucket.org/isabelle_project/isabelle-release/commits/01920e390645
so it will be in Isabelle2016-1-RC4.
At a later stage, there should be a way to specify pretty printing
length explicitly, e.g. via the new properties syntax for blocks. That
is something for the time after the release, though.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC