On 31 August 2010 18:37, Bruce Momjian <br...@momjian.us> wrote: > Thom Brown wrote: >> In a way I am. Users have the ability (although not often exercised) >> to change the default font and size. I gave the HTML tag a font-size, >> so that anything under it would be based on that. We use relative >> font sizes in our CSS, which means usually we'd be proportional to >> whatever the user had set. But what I've done is set a base size >> (17px in this case, and only in documentation) which everything else >> will be based on. So the downside is whatever the user set their >> default font size to in their browser will be ignored (or not fallen >> back to if you prefer). This doesn't, however, prevent them from >> using a text zoom (available in pretty much every web browser) to >> increase the size of all rendered fonts. >> >> The problem is, by default, Firefox sets proportional fonts to 16px, >> and monospace to 12px, so there's always a visual discrepancy when >> these fonts appear alongside one another. >> >> But the benefit of the javascript hack was that we weren't setting a >> base font size for everything, we just bump up the relative font size >> for elements which are monospaced by default. >> >> There's pros and cons to both approaches. I'm not sure which one you >> guys prefer. > > If we are using Javascript, why can't we probe the font size and do > something reasonable, e.g. make monospace larger only if it smaller than > proportional?
Hmm.. I don't know if the rendered font size is exposed to the DOM. If someone with some ECMAScript-fu knows how, we could do that. -- Thom Brown Twitter: @darkixion IRC (freenode): dark_ixion Registered Linux user: #516935 -- Sent via pgsql-docs mailing list (pgsql-docs@postgresql.org) To make changes to your subscription: http://www.postgresql.org/mailpref/pgsql-docs
