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






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