TAPAAL

Merge lp:~tapaal-contributor/tapaal/undo-shared-place-transition-1848948 into lp:tapaal

  1. undo-shared-place-transition-1848948
  2. Merge into trunk
Proposed by Peter Haahr Taankvist
Status: Merged
Approved by: Jiri Srba
Approved revision: 1020
Merged at revision: 1021
Proposed branch: lp:~tapaal-contributor/tapaal/undo-shared-place-transition-1848948
Merge into: lp:tapaal
Diff against target: 52 lines (+12/-5)
2 files modified
src/pipe/gui/widgets/PlaceEditorPanel.java (+6/-3)
src/pipe/gui/widgets/TAPNTransitionEditor.java (+6/-2)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/undo-shared-place-transition-1848948
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+374651@code.launchpad.net

Commit message

Making a place or transition shared now only requires one press on undo to undo

To post a comment you must log in.
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
1=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
2--- src/pipe/gui/widgets/PlaceEditorPanel.java 2019-03-04 13:27:40 +0000
3+++ src/pipe/gui/widgets/PlaceEditorPanel.java 2019-10-24 09:58:47 +0000
4@@ -71,6 +71,7 @@
5 private TimedPlaceComponent place;
6 private Context context;
7 private boolean makeNewShared = false;
8+ private boolean doNewEdit = true;
9
10 private Vector<TimedPlace> sharedPlaces;
11 private int maxNumberOfPlacesToShowAtOnce = 20;
12@@ -663,9 +664,11 @@
13 JOptionPane.showMessageDialog(this,"It is allowed to have at most " + Pipe.MAX_NUMBER_OF_TOKENS_ALLOWED + " tokens in a place.", "Error", JOptionPane.ERROR_MESSAGE);
14 return false;
15 }
16-
17- context.undoManager().newEdit(); // new "transaction""
18-
19+ //Only make new edit if it has not already been done
20+ if(doNewEdit) {
21+ context.undoManager().newEdit(); // new "transaction""
22+ doNewEdit = false;
23+ }
24 TimedPlace underlyingPlace = place.underlyingPlace();
25
26 SharedPlace selectedPlace = (SharedPlace)sharedPlacesComboBox.getSelectedItem();
27
28=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
29--- src/pipe/gui/widgets/TAPNTransitionEditor.java 2019-03-04 13:27:40 +0000
30+++ src/pipe/gui/widgets/TAPNTransitionEditor.java 2019-10-24 09:58:47 +0000
31@@ -46,6 +46,7 @@
32 private Context context;
33
34 private int maxNumberOfTransitionsToShowAtOnce = 20;
35+ boolean doNewEdit = true;
36
37 public TAPNTransitionEditor(JRootPane _rootPane, TimedTransitionComponent _transition, Context context) {
38 rootPane = _rootPane;
39@@ -396,8 +397,11 @@
40 if(urgentCheckBox.isSelected() && !isUrgencyOK()){
41 return false;
42 }
43-
44- context.undoManager().newEdit(); // new "transaction""
45+ //Only do new edit if it has not already been done
46+ if(doNewEdit) {
47+ context.undoManager().newEdit(); // new "transaction""
48+ doNewEdit = false;
49+ }
50
51 boolean wasShared = transition.underlyingTransition().isShared() && !sharedCheckBox.isSelected();
52 if(transition.underlyingTransition().isShared()){

Subscribers

People subscribed via source and target branches