← Back to branch summary

~tapaal-contributor/tapaal/fix-double-undo

« back to all changes in this revision

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

  • Committer: Jiri Srba
  • Date: 2021-04-09 10:13:31 UTC
  • mfrom: (1127.1.2 cut-names-1923011)
  • Revision ID: srba@cs.aau.dk-20210409101331-yovfsfk1qm8hss0v
merged in lp:~tapaal-contributor/tapaal/cut-names-1923011 fixing a problem with box heights on linux

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/PlaceEditorPanel.java
25
25
import dk.aau.cs.gui.TabContent;
26
26
import net.tapaal.swinghelpers.CustomJSpinner;
27
27
import net.tapaal.swinghelpers.GridBagHelper;
 
28
import net.tapaal.swinghelpers.SwingHelper;
28
29
import net.tapaal.swinghelpers.WidthAdjustingComboBox;
29
30
import pipe.dataLayer.Template;
30
31
import pipe.gui.CreateGui;
251
252
                basicPropertiesPanel.add(nameLabel, gridBagConstraints);
252
253
 
253
254
                nameTextField = new javax.swing.JTextField();
254
 
                nameTextField.setPreferredSize(new Dimension(290,27));
 
255
        SwingHelper.setPreferredWidth(nameTextField,290);
255
256
 
256
257
                sharedPlacesComboBox = new WidthAdjustingComboBox(maxNumberOfPlacesToShowAtOnce);
257
258
 
258
 
                sharedPlacesComboBox.setPreferredSize(new Dimension(290,27));
 
259
                SwingHelper.setPreferredWidth(sharedPlacesComboBox,290);
259
260
 
260
261
                sharedPlacesComboBox.addItemListener(e -> {
261
262
                        SharedPlace place = (SharedPlace)e.getItem();