TAPAAL

Merge lp:~tapaal-contributor/tapaal/cut-names-1923011 into lp:tapaal

  1. cut-names-1923011
  2. Merge into trunk
Proposed by Peter Haahr Taankvist
Status: Merged
Approved by: Jiri Srba
Approved revision: 1129
Merged at revision: 1128
Proposed branch: lp:~tapaal-contributor/tapaal/cut-names-1923011
Merge into: lp:tapaal
Diff against target: 321 lines (+44/-36)
11 files modified
src/dk/aau/cs/gui/SharedPlaceNamePanel.java (+2/-2)
src/dk/aau/cs/gui/SharedTransitionNamePanel.java (+2/-2)
src/dk/aau/cs/gui/TemplateExplorer.java (+6/-6)
src/net/tapaal/swinghelpers/CustomJSpinner.java (+1/-3)
src/net/tapaal/swinghelpers/SwingHelper.java (+8/-0)
src/pipe/gui/GuiFrame.java (+3/-4)
src/pipe/gui/widgets/ConstantsDialogPanel.java (+3/-3)
src/pipe/gui/widgets/GuardDialogue.java (+11/-10)
src/pipe/gui/widgets/NewTAPNPanel.java (+2/-2)
src/pipe/gui/widgets/PlaceEditorPanel.java (+3/-2)
src/pipe/gui/widgets/TAPNTransitionEditor.java (+3/-2)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/cut-names-1923011
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Kenneth Yrke Jørgensen code Approve
Review via email: mp+400775@code.launchpad.net

Commit message

Let java control height of text fields so that it works for all distributions.

To post a comment you must log in.
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

Before merging, could you make a search for something like "new Dimension(" to see if you can find other places where this could be an issue.

review: Approve (code)
Revision history for this message
Peter Haahr Taankvist (ptaank) wrote :

It happens several places, but now it only happens for buttons and panels. Should this also be changed?

Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

For now just focus on button and panels :)

Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'src/dk/aau/cs/gui/SharedPlaceNamePanel.java'
--- src/dk/aau/cs/gui/SharedPlaceNamePanel.java 2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/gui/SharedPlaceNamePanel.java 2021-04-08 08:40:30 +0000
@@ -15,6 +15,7 @@
15import javax.swing.JRootPane;15import javax.swing.JRootPane;
16import javax.swing.JTextField;16import javax.swing.JTextField;
1717
18import net.tapaal.swinghelpers.SwingHelper;
18import pipe.dataLayer.TAPNQuery;19import pipe.dataLayer.TAPNQuery;
19import dk.aau.cs.TCTL.visitors.RenameSharedPlaceVisitor;20import dk.aau.cs.TCTL.visitors.RenameSharedPlaceVisitor;
20import dk.aau.cs.gui.SharedPlacesAndTransitionsPanel.SharedPlacesListModel;21import dk.aau.cs.gui.SharedPlacesAndTransitionsPanel.SharedPlacesListModel;
@@ -80,8 +81,7 @@
80 81
81 String initialText = (placeToEdit == null) ? "" : placeToEdit.name();82 String initialText = (placeToEdit == null) ? "" : placeToEdit.name();
82 nameField = new JTextField(initialText);83 nameField = new JTextField(initialText);
83 nameField.setMinimumSize(new Dimension(330, 25));84 SwingHelper.setPreferredWidth(nameField,330);
84 nameField.setPreferredSize(new Dimension(330, 25));
85 nameField.addActionListener(e -> {85 nameField.addActionListener(e -> {
86 okButton.requestFocusInWindow();86 okButton.requestFocusInWindow();
87 okButton.doClick();87 okButton.doClick();
8888
=== modified file 'src/dk/aau/cs/gui/SharedTransitionNamePanel.java'
--- src/dk/aau/cs/gui/SharedTransitionNamePanel.java 2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/gui/SharedTransitionNamePanel.java 2021-04-08 08:40:30 +0000
@@ -15,6 +15,7 @@
15import javax.swing.JRootPane;15import javax.swing.JRootPane;
16import javax.swing.JTextField;16import javax.swing.JTextField;
1717
18import net.tapaal.swinghelpers.SwingHelper;
18import pipe.gui.undo.UndoManager;19import pipe.gui.undo.UndoManager;
19import pipe.dataLayer.TAPNQuery;20import pipe.dataLayer.TAPNQuery;
20import dk.aau.cs.TCTL.visitors.RenameSharedTransitionVisitor;21import dk.aau.cs.TCTL.visitors.RenameSharedTransitionVisitor;
@@ -86,8 +87,7 @@
86 87
87 String initialText = (transitionToEdit == null) ? "" : transitionToEdit.name();88 String initialText = (transitionToEdit == null) ? "" : transitionToEdit.name();
88 nameField = new JTextField(initialText);89 nameField = new JTextField(initialText);
89 nameField.setMinimumSize(new Dimension(330, 25));90 SwingHelper.setPreferredWidth(nameField,330);
90 nameField.setPreferredSize(new Dimension(330, 25));
91 nameField.addActionListener(e -> {91 nameField.addActionListener(e -> {
92 okButton.requestFocusInWindow();92 okButton.requestFocusInWindow();
93 okButton.doClick();93 okButton.doClick();
9494
=== modified file 'src/dk/aau/cs/gui/TemplateExplorer.java'
--- src/dk/aau/cs/gui/TemplateExplorer.java 2020-08-04 08:53:19 +0000
+++ src/dk/aau/cs/gui/TemplateExplorer.java 2021-04-08 08:40:30 +0000
@@ -39,6 +39,7 @@
39import dk.aau.cs.gui.undo.MoveElementDownCommand;39import dk.aau.cs.gui.undo.MoveElementDownCommand;
40import dk.aau.cs.gui.undo.MoveElementUpCommand;40import dk.aau.cs.gui.undo.MoveElementUpCommand;
41import net.tapaal.resourcemanager.ResourceManager;41import net.tapaal.resourcemanager.ResourceManager;
42import net.tapaal.swinghelpers.SwingHelper;
42import pipe.dataLayer.DataLayer;43import pipe.dataLayer.DataLayer;
43import pipe.dataLayer.TAPNQuery;44import pipe.dataLayer.TAPNQuery;
44import pipe.dataLayer.Template;45import pipe.dataLayer.Template;
@@ -551,9 +552,9 @@
551 nameContainer.setLayout(new GridBagLayout());552 nameContainer.setLayout(new GridBagLayout());
552 size = new Dimension(330, 25);553 size = new Dimension(330, 25);
553554
554 nameTextField = new javax.swing.JTextField(); 555 nameTextField = new javax.swing.JTextField();
555 nameTextField.setPreferredSize(size);556 SwingHelper.setPreferredWidth(nameTextField,330);
556 nameTextField.setText(nameToShow); 557 nameTextField.setText(nameToShow);
557 nameTextField.addAncestorListener(new RequestFocusListener());558 nameTextField.addAncestorListener(new RequestFocusListener());
558 nameTextField.addActionListener(e -> {559 nameTextField.addActionListener(e -> {
559 okButton.requestFocusInWindow();560 okButton.requestFocusInWindow();
@@ -659,10 +660,9 @@
659 container.setLayout(new GridBagLayout());660 container.setLayout(new GridBagLayout());
660 nameContainer = new JPanel();661 nameContainer = new JPanel();
661 nameContainer.setLayout(new GridBagLayout());662 nameContainer.setLayout(new GridBagLayout());
662 size = new Dimension(330, 25);
663663
664 nameTextField = new javax.swing.JTextField(); 664 nameTextField = new javax.swing.JTextField();
665 nameTextField.setPreferredSize(size);665 SwingHelper.setPreferredWidth(nameTextField,330);
666 nameTextField.setText(oldname);666 nameTextField.setText(oldname);
667 nameTextField.addAncestorListener(new RequestFocusListener());667 nameTextField.addAncestorListener(new RequestFocusListener());
668 nameTextField.addActionListener(e -> {668 nameTextField.addActionListener(e -> {
669669
=== modified file 'src/net/tapaal/swinghelpers/CustomJSpinner.java'
--- src/net/tapaal/swinghelpers/CustomJSpinner.java 2020-04-18 12:30:50 +0000
+++ src/net/tapaal/swinghelpers/CustomJSpinner.java 2021-04-08 08:40:30 +0000
@@ -104,9 +104,7 @@
104 ((JSpinner)e.getSource()).setValue(maximumValue);104 ((JSpinner)e.getSource()).setValue(maximumValue);
105 }105 }
106 });106 });
107 this.setPreferredSize(new Dimension(100, 25));107 SwingHelper.setPreferredWidth(this, 100);
108 this.setMaximumSize(new Dimension(100, 25));
109 this.setMinimumSize(new Dimension(100, 25));
110 108
111 final JSpinner spinner = this;109 final JSpinner spinner = this;
112110
113111
=== added file 'src/net/tapaal/swinghelpers/SwingHelper.java'
--- src/net/tapaal/swinghelpers/SwingHelper.java 1970-01-01 00:00:00 +0000
+++ src/net/tapaal/swinghelpers/SwingHelper.java 2021-04-08 08:40:30 +0000
@@ -0,0 +1,8 @@
1package net.tapaal.swinghelpers;
2import java.awt.*;
3public class SwingHelper {
4 public static void setPreferredWidth(Component c, int width) {
5 var pSize = c.getPreferredSize();
6 c.setPreferredSize(new Dimension(width, pSize.height));
7 }
8}
0\ No newline at end of file9\ No newline at end of file
110
=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java 2020-12-16 08:38:28 +0000
+++ src/pipe/gui/GuiFrame.java 2021-04-08 08:40:30 +0000
@@ -27,6 +27,7 @@
27import net.tapaal.helpers.Reference.MutableReference;27import net.tapaal.helpers.Reference.MutableReference;
28import net.tapaal.helpers.Reference.Reference;28import net.tapaal.helpers.Reference.Reference;
29import net.tapaal.swinghelpers.ExtendedJTabbedPane;29import net.tapaal.swinghelpers.ExtendedJTabbedPane;
30import net.tapaal.swinghelpers.SwingHelper;
30import net.tapaal.swinghelpers.ToggleButtonWithoutText;31import net.tapaal.swinghelpers.ToggleButtonWithoutText;
31import org.jetbrains.annotations.NotNull;32import org.jetbrains.annotations.NotNull;
32import pipe.dataLayer.TAPNQuery;33import pipe.dataLayer.TAPNQuery;
@@ -866,7 +867,7 @@
866 * for generic addition of comboboxes867 * for generic addition of comboboxes
867 */868 */
868 private void addZoomComboBox(JToolBar toolBar, Action action) {869 private void addZoomComboBox(JToolBar toolBar, Action action) {
869 Dimension zoomComboBoxDimension = new Dimension(75, 28);870 Dimension zoomComboBoxDimension = new Dimension(100, 28);
870871
871 String[] zoomExamplesStrings = new String[zoomLevels.length];872 String[] zoomExamplesStrings = new String[zoomLevels.length];
872 int i;873 int i;
@@ -878,9 +879,7 @@
878 zoomComboBox.setEditable(true);879 zoomComboBox.setEditable(true);
879 zoomComboBox.setSelectedItem("100%");880 zoomComboBox.setSelectedItem("100%");
880 zoomComboBox.setMaximumRowCount(zoomLevels.length);881 zoomComboBox.setMaximumRowCount(zoomLevels.length);
881 zoomComboBox.setMaximumSize(zoomComboBoxDimension);882 SwingHelper.setPreferredWidth(zoomComboBox,zoomComboBoxDimension.width);
882 zoomComboBox.setMinimumSize(zoomComboBoxDimension);
883 zoomComboBox.setPreferredSize(zoomComboBoxDimension);
884 zoomComboBox.setAction(action);883 zoomComboBox.setAction(action);
885 zoomComboBox.setFocusable(false);884 zoomComboBox.setFocusable(false);
886 toolBar.add(zoomComboBox);885 toolBar.add(zoomComboBox);
887886
=== modified file 'src/pipe/gui/widgets/ConstantsDialogPanel.java'
--- src/pipe/gui/widgets/ConstantsDialogPanel.java 2020-07-20 09:36:10 +0000
+++ src/pipe/gui/widgets/ConstantsDialogPanel.java 2021-04-08 08:40:30 +0000
@@ -17,6 +17,7 @@
1717
18import net.tapaal.swinghelpers.CustomJSpinner;18import net.tapaal.swinghelpers.CustomJSpinner;
19import net.tapaal.swinghelpers.RequestFocusListener;19import net.tapaal.swinghelpers.RequestFocusListener;
20import net.tapaal.swinghelpers.SwingHelper;
20import pipe.gui.CreateGui;21import pipe.gui.CreateGui;
21import dk.aau.cs.gui.undo.Command;22import dk.aau.cs.gui.undo.Command;
22import dk.aau.cs.model.tapn.Constant;23import dk.aau.cs.model.tapn.Constant;
@@ -75,9 +76,8 @@
75 private void initComponents() {76 private void initComponents() {
76 container = new JPanel();77 container = new JPanel();
77 container.setLayout(new GridBagLayout());78 container.setLayout(new GridBagLayout());
78 size = new Dimension(330, 25);79 nameTextField = new javax.swing.JTextField();
79 nameTextField = new javax.swing.JTextField(); 80 SwingHelper.setPreferredWidth(nameTextField,330);
80 nameTextField.setPreferredSize(size);
81 nameTextField.addAncestorListener(new RequestFocusListener());81 nameTextField.addAncestorListener(new RequestFocusListener());
82 nameTextField.addActionListener(e -> {82 nameTextField.addActionListener(e -> {
83 okButton.requestFocusInWindow();83 okButton.requestFocusInWindow();
8484
=== modified file 'src/pipe/gui/widgets/GuardDialogue.java'
--- src/pipe/gui/widgets/GuardDialogue.java 2020-09-24 15:33:08 +0000
+++ src/pipe/gui/widgets/GuardDialogue.java 2021-04-08 08:40:30 +0000
@@ -29,6 +29,7 @@
2929
30import dk.aau.cs.gui.TabContent;30import dk.aau.cs.gui.TabContent;
31import dk.aau.cs.model.tapn.*;31import dk.aau.cs.model.tapn.*;
32import net.tapaal.swinghelpers.SwingHelper;
32import net.tapaal.swinghelpers.WidthAdjustingComboBox;33import net.tapaal.swinghelpers.WidthAdjustingComboBox;
33import pipe.gui.CreateGui;34import pipe.gui.CreateGui;
34import pipe.gui.graphicElements.PetriNetObject;35import pipe.gui.graphicElements.PetriNetObject;
@@ -233,11 +234,11 @@
233 gridBagConstraints.anchor = GridBagConstraints.WEST;234 gridBagConstraints.anchor = GridBagConstraints.WEST;
234 gridBagConstraints.insets = new Insets(3, 3, 3, 3);235 gridBagConstraints.insets = new Insets(3, 3, 3, 3);
235 weightEditPanel.add(label, gridBagConstraints);236 weightEditPanel.add(label, gridBagConstraints);
236 237
237 Dimension intervalBoxDims = new Dimension(190, 25);238 Dimension intervalBoxDims = new Dimension(190, 25);
238239
239 weightNumber = new JSpinner();240 weightNumber = new JSpinner();
240 weightNumber.setPreferredSize(intervalBoxDims);241 SwingHelper.setPreferredWidth(weightNumber,intervalBoxDims.width);
241 weightNumber.addChangeListener(e -> {242 weightNumber.addChangeListener(e -> {
242 if((Integer) weightNumber.getValue() < 1){243 if((Integer) weightNumber.getValue() < 1){
243 weightNumber.setValue(1);244 weightNumber.setValue(1);
@@ -271,8 +272,8 @@
271 weightConstantsComboBox.setModel(new DefaultComboBoxModel<>(constantArray));272 weightConstantsComboBox.setModel(new DefaultComboBoxModel<>(constantArray));
272 weightConstantsComboBox.setMaximumRowCount(20);273 weightConstantsComboBox.setMaximumRowCount(20);
273 weightConstantsComboBox.setVisible(false);274 weightConstantsComboBox.setVisible(false);
274 weightConstantsComboBox.setPreferredSize(intervalBoxDims);275 SwingHelper.setPreferredWidth(weightConstantsComboBox,intervalBoxDims.width);
275 276
276 gridBagConstraints = new GridBagConstraints();277 gridBagConstraints = new GridBagConstraints();
277 gridBagConstraints.gridx = 1;278 gridBagConstraints.gridx = 1;
278 gridBagConstraints.gridy = 1;279 gridBagConstraints.gridy = 1;
@@ -379,7 +380,7 @@
379 firstIntervalNumber = new JSpinner();380 firstIntervalNumber = new JSpinner();
380 // firstIntervalNumber.setMaximumSize(intervalBoxDims);381 // firstIntervalNumber.setMaximumSize(intervalBoxDims);
381 // firstIntervalNumber.setMinimumSize(intervalBoxDims);382 // firstIntervalNumber.setMinimumSize(intervalBoxDims);
382 firstIntervalNumber.setPreferredSize(intervalBoxDims);383 SwingHelper.setPreferredWidth(firstIntervalNumber,intervalBoxDims.width);
383 firstIntervalNumber.addChangeListener(this::firstSpinnerStateChanged);384 firstIntervalNumber.addChangeListener(this::firstSpinnerStateChanged);
384 GridBagConstraints gridBagConstraints = new GridBagConstraints();385 GridBagConstraints gridBagConstraints = new GridBagConstraints();
385 gridBagConstraints.gridx = 2;386 gridBagConstraints.gridx = 2;
@@ -393,9 +394,8 @@
393 guardEditPanel.add(new JLabel(" , "), gridBagConstraints);394 guardEditPanel.add(new JLabel(" , "), gridBagConstraints);
394395
395 secondIntervalNumber = new JSpinner();396 secondIntervalNumber = new JSpinner();
396 secondIntervalNumber.setMaximumSize(intervalBoxDims);397
397 secondIntervalNumber.setMinimumSize(intervalBoxDims);398 SwingHelper.setPreferredWidth(secondIntervalNumber,intervalBoxDims.width);
398 secondIntervalNumber.setPreferredSize(intervalBoxDims);
399 secondIntervalNumber.addChangeListener(this::secondSpinnerStateChanged);399 secondIntervalNumber.addChangeListener(this::secondSpinnerStateChanged);
400400
401 gridBagConstraints.gridx = 4;401 gridBagConstraints.gridx = 4;
@@ -430,7 +430,8 @@
430 leftConstantsComboBox.setVisible(false);430 leftConstantsComboBox.setVisible(false);
431 // leftConstantsComboBox.setMaximumSize(intervalBoxDims);431 // leftConstantsComboBox.setMaximumSize(intervalBoxDims);
432 // leftConstantsComboBox.setMinimumSize(intervalBoxDims);432 // leftConstantsComboBox.setMinimumSize(intervalBoxDims);
433 leftConstantsComboBox.setPreferredSize(intervalBoxDims);433 SwingHelper.setPreferredWidth(leftConstantsComboBox,intervalBoxDims.width);
434 //leftConstantsComboBox.setPreferredSize(intervalBoxDims);
434 leftConstantsComboBox.addItemListener(e -> {435 leftConstantsComboBox.addItemListener(e -> {
435 if (e.getStateChange() == ItemEvent.SELECTED) {436 if (e.getStateChange() == ItemEvent.SELECTED) {
436 updateRightConstantComboBox();437 updateRightConstantComboBox();
@@ -462,7 +463,7 @@
462 rightConstantsComboBox.setVisible(false);463 rightConstantsComboBox.setVisible(false);
463 // rightConstantsComboBox.setMaximumSize(intervalBoxDims);464 // rightConstantsComboBox.setMaximumSize(intervalBoxDims);
464 // rightConstantsComboBox.setMinimumSize(intervalBoxDims);465 // rightConstantsComboBox.setMinimumSize(intervalBoxDims);
465 rightConstantsComboBox.setPreferredSize(intervalBoxDims);466 SwingHelper.setPreferredWidth(rightConstantsComboBox,intervalBoxDims.width);
466 gridBagConstraints = new GridBagConstraints();467 gridBagConstraints = new GridBagConstraints();
467 rightConstantsComboBox.addItemListener(e -> {468 rightConstantsComboBox.addItemListener(e -> {
468 if (e.getStateChange() == ItemEvent.SELECTED) {469 if (e.getStateChange() == ItemEvent.SELECTED) {
469470
=== modified file 'src/pipe/gui/widgets/NewTAPNPanel.java'
--- src/pipe/gui/widgets/NewTAPNPanel.java 2020-08-04 08:53:19 +0000
+++ src/pipe/gui/widgets/NewTAPNPanel.java 2021-04-08 08:40:30 +0000
@@ -11,6 +11,7 @@
11import javax.swing.*;11import javax.swing.*;
1212
13import dk.aau.cs.gui.TabContent;13import dk.aau.cs.gui.TabContent;
14import net.tapaal.swinghelpers.SwingHelper;
14import pipe.gui.CreateGui;15import pipe.gui.CreateGui;
15import pipe.gui.Grid;16import pipe.gui.Grid;
16import pipe.gui.GuiFrame;17import pipe.gui.GuiFrame;
@@ -127,8 +128,7 @@
127 String defaultName = String.format("New Petri net %1$d", frame128 String defaultName = String.format("New Petri net %1$d", frame
128 .getNameCounter());129 .getNameCounter());
129 nameTextBox = new JTextField(defaultName);130 nameTextBox = new JTextField(defaultName);
130 Dimension size = new Dimension(330, 25); 131 SwingHelper.setPreferredWidth(nameTextBox,330);
131 nameTextBox.setPreferredSize(size);
132 gbc = new GridBagConstraints();132 gbc = new GridBagConstraints();
133 gbc.gridx = 1;133 gbc.gridx = 1;
134 gbc.gridy = 0;134 gbc.gridy = 0;
135135
=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
--- src/pipe/gui/widgets/PlaceEditorPanel.java 2020-08-10 09:34:06 +0000
+++ src/pipe/gui/widgets/PlaceEditorPanel.java 2021-04-08 08:40:30 +0000
@@ -25,6 +25,7 @@
25import dk.aau.cs.gui.TabContent;25import dk.aau.cs.gui.TabContent;
26import net.tapaal.swinghelpers.CustomJSpinner;26import net.tapaal.swinghelpers.CustomJSpinner;
27import net.tapaal.swinghelpers.GridBagHelper;27import net.tapaal.swinghelpers.GridBagHelper;
28import net.tapaal.swinghelpers.SwingHelper;
28import net.tapaal.swinghelpers.WidthAdjustingComboBox;29import net.tapaal.swinghelpers.WidthAdjustingComboBox;
29import pipe.dataLayer.Template;30import pipe.dataLayer.Template;
30import pipe.gui.CreateGui;31import pipe.gui.CreateGui;
@@ -251,11 +252,11 @@
251 basicPropertiesPanel.add(nameLabel, gridBagConstraints);252 basicPropertiesPanel.add(nameLabel, gridBagConstraints);
252253
253 nameTextField = new javax.swing.JTextField();254 nameTextField = new javax.swing.JTextField();
254 nameTextField.setPreferredSize(new Dimension(290,27));255 SwingHelper.setPreferredWidth(nameTextField,290);
255256
256 sharedPlacesComboBox = new WidthAdjustingComboBox(maxNumberOfPlacesToShowAtOnce);257 sharedPlacesComboBox = new WidthAdjustingComboBox(maxNumberOfPlacesToShowAtOnce);
257258
258 sharedPlacesComboBox.setPreferredSize(new Dimension(290,27));259 SwingHelper.setPreferredWidth(sharedPlacesComboBox,290);
259260
260 sharedPlacesComboBox.addItemListener(e -> {261 sharedPlacesComboBox.addItemListener(e -> {
261 SharedPlace place = (SharedPlace)e.getItem();262 SharedPlace place = (SharedPlace)e.getItem();
262263
=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
--- src/pipe/gui/widgets/TAPNTransitionEditor.java 2020-08-10 09:34:06 +0000
+++ src/pipe/gui/widgets/TAPNTransitionEditor.java 2021-04-08 08:40:30 +0000
@@ -18,6 +18,7 @@
18import javax.swing.event.CaretListener;18import javax.swing.event.CaretListener;
19import net.tapaal.swinghelpers.GridBagHelper;19import net.tapaal.swinghelpers.GridBagHelper;
20import dk.aau.cs.gui.undo.*;20import dk.aau.cs.gui.undo.*;
21import net.tapaal.swinghelpers.SwingHelper;
21import net.tapaal.swinghelpers.WidthAdjustingComboBox;22import net.tapaal.swinghelpers.WidthAdjustingComboBox;
22import pipe.gui.CreateGui;23import pipe.gui.CreateGui;
23import pipe.gui.graphicElements.tapn.TimedTransitionComponent;24import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
@@ -66,7 +67,7 @@
66 transitionEditorPanel = new JPanel();67 transitionEditorPanel = new JPanel();
67 nameLabel = new JLabel();68 nameLabel = new JLabel();
68 nameTextField = new JTextField();69 nameTextField = new JTextField();
69 nameTextField.setPreferredSize(new Dimension(290,27));70 SwingHelper.setPreferredWidth(nameTextField, 290);
70 rotationLabel = new JLabel();71 rotationLabel = new JLabel();
71 rotationComboBox = new JComboBox<>();72 rotationComboBox = new JComboBox<>();
72 buttonPanel = new JPanel();73 buttonPanel = new JPanel();
@@ -80,7 +81,7 @@
8081
8182
82 sharedTransitionsComboBox = new WidthAdjustingComboBox<>(maxNumberOfTransitionsToShowAtOnce);83 sharedTransitionsComboBox = new WidthAdjustingComboBox<>(maxNumberOfTransitionsToShowAtOnce);
83 sharedTransitionsComboBox.setPreferredSize(new Dimension(290,27));84 SwingHelper.setPreferredWidth(sharedTransitionsComboBox,290);
84 sharedTransitionsComboBox.addActionListener(e -> {85 sharedTransitionsComboBox.addActionListener(e -> {
85 if(((SharedTransition)sharedTransitionsComboBox.getSelectedItem()).transitions().isEmpty()){86 if(((SharedTransition)sharedTransitionsComboBox.getSelectedItem()).transitions().isEmpty()){
86 ((SharedTransition)sharedTransitionsComboBox.getSelectedItem()).setUrgent(urgentCheckBox.isSelected());87 ((SharedTransition)sharedTransitionsComboBox.getSelectedItem()).setUrgent(urgentCheckBox.isSelected());

Subscribers

People subscribed via source and target branches