#335 Title fontsize cannot be changed

[Gerard Borg]

On Ubuntu 24.04.4 LTS running

Minsky 3.28.1
Minsky GUI 3.28.1
Ravel 2.5.6-pro: Expires in 74 days
Angular 21.2.17

Options->Preferences does not show a global fontSize option.

There does not seem to be a .~/.minsky or ~/.config/minsky.ini file on my system.

The consequence is that the Godley table title font is too small to be legible.

[High Performance Coder]

For reference, the preferences file is stored in ~/.config/minsky/config.json

Yes - it make sense there should be a way of specifying the default font size, rather than assuming the system provides a sensible default.

But this is more of a feature than a bug, so I'm moving it to the feature request stack.

[High Performance Coder]

Ticket moved from /p/minsky/tickets/1951/

Can't be converted:

• _priority: 4normal

[Gerard Borg]

For reference on my system it is ~/.config/minsky-electron/config.json

I edited this file to change the Godley title font using various approaches like...

"preferences": {
    "godleyTableOutputStyle": "sign",
    "enableMultipleEquityColumns": false,
    "numberOfRecentFilesToDisplay": 10,
    "wrapLongEquationsInLatexExport": false,
    "font": "FontAwesome",
    "fontSize": 24,
    "numBackups": 1
},

or

"preferences": {
    "godleyTableOutputStyle": "sign",
    "enableMultipleEquityColumns": false,
    "numberOfRecentFilesToDisplay": 10,
    "wrapLongEquationsInLatexExport": false,
    "font": "FontAwesome",
    "fontSizes": [
        {
            "name": "Small",
            "slug": "small",
            "size": "13px"
        },
        {
            "name": "Large",
            "slug": "large",
            "size": "24px"
        }
    ],

Each time I rerun Ravel to read the new config.json. But none of this works.

[High Performance Coder]

It won't. That file is just used to stash the preferences set in the control panel. Setting the default font size just isn't implemented. Originally, the idea was that the operating system would provide whatever font and size was suitable, and we'd use that. Adding the ability to select fonts became necessary when it was discovered that Windows tended to use rather Unicode deficient fontsets by default.

That said, the Godley table popup window is rendered in the Chromium engine, so that would have a completely different set of options for setting them (via CSS most likely).