Whew! Glad I got it right this time :-). As for your questions, I'll
defer to those who actually might know the answers but on Windows, the
IE and Edge browsers allow for "scaling" (not sure that this is the
right term) the display. In my case, I almost always have it set 125%,
making the displayed image easier for me to read. Unfortunately, some
sites don't scale very well and I have to go back to 100% in order to
see fields with which I need to interact. So it would seem that we are
really only talking about the default starting font size for the ooRexx
documentation and whether it is better to have a smaller value (that the
user can enlarge if he wishes using his browser's controls) or a larger
value so he doesn't need to do anything with it most of the time. And,
of course, everyone will have their own preference so I don't expect a
consensus here, just a majority opinion for guidance.
Gil
On 3/10/2020 2:11 PM, Jeremy Nicoll wrote:
On Tue, 10 Mar 2020, at 17:15, Gil Barmwater wrote:
OK, I believe I have it right this time! Here is the original, smaller
<https://www.dropbox.com/s/lqv49jl2obgwxjn/rxmath-original.zip?dl=0>
version as well as the newer, larger
<https://www.dropbox.com/s/f48m470358i6ai0/rxmath-bigger.zip?dl=0>
version. All comments are appreciated.
That's better! I certainly prefer the larger text.
I notice that in the CSS, you changed the old font size from "12px" to "0.9em".
Does that (also?) have an implication for users of high-dpi screeens, where the
old size 12 pixels would perhaps now be very small? I'm assuming that 0.9 em
means 90% of the width of a lower-case "m" in whatever font is selected for a
piece of text?
I'm not using a high dpi screen. If I were, I don't know if I'd want an even
bigger
default size. Does the default font get set up only by the CSS, or also by the
user's browser? And if the latter, on a high dpi system, does screen scaling
(at
the OS or window manager level) influence this?
I've used websites in the past which had (typically) a display of three "A"s in
one
corner - a small one, medium one, and a larger one; clicking on one would set
sometimes a specific small, medium and large font size, or in some cases allow
successive shrinking or expanding of the displayed text size. I'm not sure if
that's
possible without using Javascript though. /If/ there's a compact piece of JS
that
would so that, it might be worth embedding it on each page, provided that there
is a fallback for browsers that don't support JS, to pick a sensible initial
display
size.
It might also be sensible to include in the shipped CSS file several settings of
font-size with adjacent comments, and tell people that they can readily change
the size in their CSS file to achieve a permanent change.
--
Gil Barmwater
_______________________________________________
Oorexx-devel mailing list
Oorexx-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/oorexx-devel
