← Back to branch summary

~tapaal-contributor/tapaal/undo-shared-place-transition-1848948

« back to all changes in this revision

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

  • Committer: ptaankvist at gmail
  • Date: 2019-10-24 09:55:33 UTC
  • Revision ID: ptaankvist@gmail.com-20191024095533-ieg33kgc37hv0dlg
https://launchpad.net/bugs/1848948
making place/transition shared now only requires one undo to undo

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/PlaceEditorPanel.java
71
71
        private TimedPlaceComponent place;
72
72
        private Context context;
73
73
        private boolean makeNewShared = false;
 
74
        private boolean doNewEdit = true;
74
75
        
75
76
        private Vector<TimedPlace> sharedPlaces;
76
77
        private int maxNumberOfPlacesToShowAtOnce = 20;
663
664
                        JOptionPane.showMessageDialog(this,"It is allowed to have at most " + Pipe.MAX_NUMBER_OF_TOKENS_ALLOWED + " tokens in a place.", "Error", JOptionPane.ERROR_MESSAGE);
664
665
                        return false;
665
666
                }
666
 
 
667
 
                context.undoManager().newEdit(); // new "transaction""
668
 
 
 
667
                //Only make new edit if it has not already been done
 
668
                if(doNewEdit) {
 
669
                        context.undoManager().newEdit(); // new "transaction""
 
670
                        doNewEdit = false;
 
671
                }
669
672
                TimedPlace underlyingPlace = place.underlyingPlace();
670
673
 
671
674
                SharedPlace selectedPlace = (SharedPlace)sharedPlacesComboBox.getSelectedItem();