[isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.

[Makarius]

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


 	Makarius