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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
