The current-render-pict-adjust functionality isn't really designed to work around your disagreements with font designers about how much space they put around letter forms. :) .... or am I misinterpreting your comment? If that's really an accurate characterization, then you might actually try just hacking the font itself?
As for current-render-pict-adjust, I can't really be sure without seeing some Redex code, but I guess what's happening is that the equal sign that's being added isn't getting the negative inset. And current-render-pict-adjust is designed to let you interpose on the bits that come from your model. If that theory is right, you might try using current-text. hth, Robby On Fri, Jun 24, 2016 at 11:36 AM, 'William J. Bowman' via Racket Users <[email protected]> wrote: > On Thu, Jun 02, 2016 at 11:40:14PM -0400, 'William J. Bowman' via Racket > Users wrote: >> Attached are two screenshots of part of a model I've extracted from Redex. >> >> The first is after changing the default fonts. As you can see, there is a >> *lot* of vertical whitespace >> around each judgment form clause and where clause. In particular, the top of >> the bounding box seems >> too high. >> >> The second is after using current-render-pict-adjust to add a negative inset >> on everything. >> It is better, but does not seem to affect the where clauses. > FYI, I found that `current-render-pict-adjust` did not affect `where` > clauses. By redefining > `where-combine`, too, to add a negative inset, I got the desired result > without the extra whitespace. > > Should `current-render-pict-adjust` affect `where-combine`, i.e., is this a > bug? > > -- > William J. Bowman > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
