I am on Windows 8.1, running Python 3.3.5 with PyQt4-4.10.4-gpl-Py3.3-Qt4.8.5-x64. I am using Leo 4.11 final, build 6240.
I have partially obtained the color combination I was looking for, simply by importing Terry's solarized theme which takes care of most things. However, this is not to say that I have solved the difficulties related to the UI configuration. I am still in the dark as to how settings should be properly managed. It's really infuriating, especially when you change a setting and for some reason it does not take effect. For instance, based on Terry's dark (solarized) theme 0, which I am trying to modify: I am now trying to change the background color of the minibuffer's edit line, to make it stand out from the surrounding background color. So, I go to the node mini-buffer & status (under stylesheet & source) and I edit the background-color parameter, setting it to another color (drastically different, so I can easily see if the change took place). Then I save and restart Leo, and the change did not take effect! (despite having been saved correctly). I am wondering: is there any other setting which overrides this?!? This is a common problem in Leo settings, from what I understand (as I encountered it in other settings). The user is likely to mad if he has to check and counter-check all these cross-referenced settings! Anyway, these are just some the difficulties I am encountering in changing the settings. I believe a radical restucturing of the way settings are handled, or at least presented to the end-user, is really called for here. There is no point in Leo being totally configurable if the user cannot manage to change even the simplest settings like the UI colors! -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/d/optout.
