← Back to branch summary

~tapaal-contributor/tapaal/display-shared-places-transitions-1879126

« back to all changes in this revision

Viewing changes to src/net/tapaal/swinghelpers/JSplitPaneFix.java

  • Committer: Jiri Srba
  • Date: 2020-04-28 19:15:28 UTC
  • mfrom: (998.2.376 testbranch)
  • Revision ID: srba@cs.aau.dk-20200428191528-3xxjqa1r4jcob5ur
merged in lp:~yrke/tapaal/testbranch doing majour refactoring of the GUI

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/net/tapaal/swinghelpers/JSplitPaneFix.java
 
1
package net.tapaal.swinghelpers;
 
2
 
 
3
import java.awt.Component;
 
4
import java.awt.Graphics;
 
5
 
 
6
import javax.swing.JSplitPane;
 
7
 
 
8
public class JSplitPaneFix extends JSplitPane {
 
9
 
 
10
        /**
 
11
         * 
 
12
         */
 
13
        private static final long serialVersionUID = -4493433117542095206L;
 
14
        private boolean isPainted;
 
15
        private boolean hasProportionalLocation;
 
16
        private double proportionalLocation;
 
17
 
 
18
        public JSplitPaneFix(int verticalSplit, Component component1, Component component2) {
 
19
                super(verticalSplit, component1, component2);
 
20
 
 
21
        }
 
22
 
 
23
        public JSplitPaneFix(int verticalSplit) {
 
24
                super(verticalSplit);
 
25
        }
 
26
 
 
27
        @Override
 
28
        public void setDividerLocation(double proportionalLocation) {
 
29
                if (!isPainted) {
 
30
                        hasProportionalLocation = true;
 
31
                        this.proportionalLocation = proportionalLocation;
 
32
                } else
 
33
                        super.setDividerLocation(proportionalLocation);
 
34
        }
 
35
 
 
36
        @Override
 
37
        public void paint(Graphics g) {
 
38
                if (!isPainted) {
 
39
                        if (hasProportionalLocation)
 
40
                                super.setDividerLocation(proportionalLocation);
 
41
                        isPainted = true;
 
42
                }
 
43
                super.paint(g);
 
44
        }
 
45
 
 
46
}