GUI textinput inconveniences #15

1. The application must be restarted for font changes to take effect.
2. Font changes don't affect the size of the glyphs on the glyph bar.
3. There's no way to type the prefix key itself, which makes it less of a changeable setting: I wanted ,円 but I can't type @\u0 with that prefix.
4. The cursor can leave the editable area and then doesn't return except by a precise click. The first impression is that the app is broken and unresponsive. Even clicking just after the ⊢ prompt will lead to this. Since trying to enter text does nothing currently in this state, I suggest that typing anything return the cursor to the end of the editable area

Thank you for this report. The behaviour when the cursor is outside the input area is indeed problematic. I will try some solutions.

As for entering the prefix itself, it should work if you type the prefix followed by space. Did you try this?

I've now changed the behaviour so that one can type anywhere. The cursor will automatically move to the input area if necessary. This fix was implemented in: ce7525181f

As for font changes, the change does take effect immediately but only newly added text. Try typing a command in the REPL after changing the font, and the new size should be seen. The reason has to do with some limitations of the underlying text component that is used, so fixing this is actually a bit trickier than one might think.

I never tried prefix-space. That works for me.