Re: [isabelle] \<^latex>

On 25/11/16 12:56, Tobias Nipkow wrote:
> 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?

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
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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.