← Back to branch summary

~tapaal-contributor/tapaal/unselect-objects-after-undo-1894108

« back to all changes in this revision

Viewing changes to src/pipe/gui/widgets/TAPNTransitionEditor.java

  • Committer: srba.jiri at gmail
  • Date: 2020-08-19 12:02:28 UTC
  • mfrom: (1071.2.34 untimed-timed-gui)
  • Revision ID: srba.jiri@gmail.com-20200819120228-ktxdev3ou3kuj3l0
merged in lp:~tapaal-contributor/tapaal/untimed-timed-gui adding timed/untimed lens projection

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/TAPNTransitionEditor.java
16
16
import javax.swing.JRootPane;
17
17
import javax.swing.JTextField;
18
18
import javax.swing.event.CaretListener;
19
 
 
20
 
 
21
19
import net.tapaal.swinghelpers.GridBagHelper;
22
20
import dk.aau.cs.gui.undo.*;
23
21
import net.tapaal.swinghelpers.WidthAdjustingComboBox;
52
50
                transition = _transition;
53
51
                this.context = context;
54
52
                initComponents();
55
 
 
 
53
        hideTimedInformation();
56
54
                rootPane.setDefaultButton(okButton);
57
55
        }
58
56
 
 
57
        private void hideTimedInformation(){
 
58
            if(!transition.isTimed()) {
 
59
            urgentCheckBox.setVisible(false);
 
60
        }
 
61
    }
 
62
 
59
63
        private void initComponents() {
60
64
                GridBagConstraints gridBagConstraints;
61
65