mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-13 09:19:13 +07:00
Fix splitter proportion (take divider size into account, it may be ~30px in Diff panel)
This commit is contained in:
@@ -57,7 +57,7 @@ public class Splitter extends JPanel {
|
||||
private final float myMaxProp;
|
||||
|
||||
|
||||
protected float myProportion;// first size divided by total size
|
||||
protected float myProportion;// first size divided by (first + second)
|
||||
|
||||
private final Divider myDivider;
|
||||
private JComponent mySecondComponent;
|
||||
@@ -261,7 +261,7 @@ public class Splitter extends JPanel {
|
||||
d = total;
|
||||
}
|
||||
else {
|
||||
size1 = myProportion * total;
|
||||
size1 = myProportion * (total - d);
|
||||
double size2 = total - size1 - d;
|
||||
|
||||
if (isHonorMinimumSize()) {
|
||||
|
||||
Reference in New Issue
Block a user