[isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.
makarius at sketis.net
Thu Mar 21 17:17:01 CET 2013
On Thu, 21 Mar 2013, Makarius wrote:
>> * "pretty.scala" currently uses "space-widths" as its internal unit.
>> It may be beneficial to refactor this to use an arbitrary unit
>> internally (chosen by the caller) and measure the space strings it
>> generates (also updating "pretty.ML" to match). This would prevent
>> the current dance of needing to divide out the width of a space
> Can you say more directly what you think that is actually wrong? As long as
> rounding is done properly (which is not necessarily the case) any unit should
> work. Java also uses floating point in some interfaces, while integer pixels
> in other spots. Both can lead to problems, but I prefer to delegate
> calculations to floating point arithmetic if possible.
See also 18120e26f818 and a981a5c8a505 as a result of looking once more --
this is not the first time nor the last time.
More information about the isabelle-dev