terminal: change font size dynamically

[hoihu]

With this change, the font size is proportional to the viewport, it scales if the browser window is resized.

This helps on high-resolution screens (tested on safari and chrome).

[pfalcon]

I actually thought about allowing to switch to bigger terminal size than 80x24, and wonder how this change would interact with that.

[hoihu]

It leaves the terminal to 80x24 and just scales the font size.

But auto-resizing the terminal window might also be possible (maybe by using a javascript function).

[dpgeorge]

You can use ctrl-+ and ctrl-- to change font size, as usual for web pages. Isn't that a better solution?

Then we can make the rows and columns expand to fill the screen, and it'll work for any font size that the user chooses.

[dpgeorge]

See #6 for an auto resizing patch.

[hoihu]

can use ctrl-+ and ctrl-- to change font size,

to have a decent "default viewing" size was the goal. Having it set in pixels is IMO not correct but then I'm not a web expert.

using ctrl+ strikes me as not really user friendly.

[dpgeorge]

to have a decent "default viewing" size was the goal.

Do you mean terminal size (cols and rows) or font size, or both?

What do you think of #6 (see http://micropython.org/webrepl/index2.html)? How to reconcile an auto font size with auto terminal size?

[hoihu]

i havent tested it (still sitting in the train..) but looking forward to trying it out!

[pfalcon]

Having it set in pixels is IMO not correct but then I'm not a web expert.

If it's set in pixels, it comes from the term.js example, that's it. Per #6 (comment) we (I) welcome anyone to make it better, but well, please show/explain that your changes don't make it worse instead (in some sense of "worse"). I'd personally prefer that there was prototyping of file xfer functionality rather than global look&feel changes, which them may need to be changed again (because currently it's too easy to assume "there's terminal widget there, and nothing else").

[hoihu]

If it's set in pixels, it comes from the term.js example, that's it

I have made a remark in #6 about that. Yes it's in term.js as default but can be overridden in the html file.

[pfalcon]

I'm not sure I made myself clear - both term.js and majority of webrepl.html come from upstream "term.js" project distribution. If it's set to 11px, it's not because I set it to that, it's because the "term.js" maintainer set it to that, and by default, s/he had a good reason to do so. If you think that another value is better, you in general would need to argue why (it's more or less clear in the case of font size, but still requires testing on various devices, in other cases, it may be less clear).

[martinlombana]

Yeah, in my case, currently, the font is very small, and I am on a 29 inches Dell monitor (not hight dpi, just regular). But if I change the term.js fontsize, then it messes up the overall structure.