Hi Cyril,
From what I read in an older P7 image
DockingBarMorph>>defaultBorderWidth was not implemented, and inherited,
from AlignmentMorph which defaultBorderWidth returns 0.
Next, why docking bar should have the same width as menu?
The question is do we want docking bar to have border?
I see the Playground tool bar is impacted, although it does not make is
UI less suitable.
In the meantime I just set DockingBarMorph>>defaultBorderWidth to
returns 0, so I can use the last build at school with students. By doing
so I did not notice glitch..
I am not sure docking bar not having border should be considered as a bug..
Thanks
Hilaire
Le 09/06/2018 à 12:38, Cyril Ferlicot a écrit :
DockingBarMorph>>defaultBorderWidth
^ self theme menuBorderWidth
I found the PR I did.
This code was already here but in another method.
The difference is that now #themeChanged take the borderWidth into
account. Before it ignored it. So it's probably that before there was
a bug where the docking bar did not matched the theme for the border
and it was corrected. Now, without the bug, you found that the theme
was not as good as you wanted and we need to update the theme.
--
Dr. Geo
http://drgeo.eu
