TAPAAL

Merge lp:~tapaal-contributor/tapaal/undo-up-down-sidepane-3.6-1870894 into lp:tapaal/3.6

  1. undo-up-down-sidepane-3.6-1870894
  2. Merge into 3.6
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 1051
Merged at revision: 1052
Proposed branch: lp:~tapaal-contributor/tapaal/undo-up-down-sidepane-3.6-1870894
Merge into: lp:tapaal/3.6
Diff against target: 433 lines (+224/-40)
7 files modified
src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java (+38/-20)
src/dk/aau/cs/gui/TemplateExplorer.java (+31/-10)
src/dk/aau/cs/gui/undo/MoveElementDownCommand.java (+46/-0)
src/dk/aau/cs/gui/undo/MoveElementUpCommand.java (+51/-0)
src/pipe/gui/widgets/ConstantsPane.java (+26/-6)
src/pipe/gui/widgets/QueryPane.java (+23/-4)
src/pipe/gui/widgets/SidePane.java (+9/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/undo-up-down-sidepane-3.6-1870894
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+384060@code.launchpad.net
To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

Next time propose the merge for 3.6 series and not for trunk.

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/SharedPlacesAndTransitionsPanel.java'
--- src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2019-03-02 11:14:31 +0000
+++ src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2020-05-16 08:49:46 +0000
@@ -30,10 +30,12 @@
30import pipe.gui.CreateGui;30import pipe.gui.CreateGui;
31import pipe.gui.undo.UndoManager;31import pipe.gui.undo.UndoManager;
32import pipe.gui.widgets.EscapableDialog;32import pipe.gui.widgets.EscapableDialog;
3333import pipe.gui.widgets.SidePane;
34import dk.aau.cs.gui.components.NonsearchableJList;34import dk.aau.cs.gui.components.NonsearchableJList;
35import dk.aau.cs.gui.undo.AddSharedPlaceCommand;35import dk.aau.cs.gui.undo.AddSharedPlaceCommand;
36import dk.aau.cs.gui.undo.Command;36import dk.aau.cs.gui.undo.Command;
37import dk.aau.cs.gui.undo.MoveElementDownCommand;
38import dk.aau.cs.gui.undo.MoveElementUpCommand;
37import dk.aau.cs.gui.undo.SortSharedPlacesCommand;39import dk.aau.cs.gui.undo.SortSharedPlacesCommand;
38import dk.aau.cs.gui.undo.SortSharedTransitionsCommand;40import dk.aau.cs.gui.undo.SortSharedTransitionsCommand;
39import dk.aau.cs.model.tapn.SharedPlace;41import dk.aau.cs.model.tapn.SharedPlace;
@@ -42,7 +44,7 @@
42import dk.aau.cs.util.Require;44import dk.aau.cs.util.Require;
43import dk.aau.cs.util.RequireException;45import dk.aau.cs.util.RequireException;
4446
45public class SharedPlacesAndTransitionsPanel extends JPanel {47public class SharedPlacesAndTransitionsPanel extends JPanel implements SidePane{
46 private static final String TRANSITION_IS_USED_MESSAGE = "<html>The shared transition is used in one or more components.<br/>TAPAAL will unshare all transitions under this name,<br/>but leave the transitions in the components.</html>";48 private static final String TRANSITION_IS_USED_MESSAGE = "<html>The shared transition is used in one or more components.<br/>TAPAAL will unshare all transitions under this name,<br/>but leave the transitions in the components.</html>";
47 private static final String PLACE_IS_USED_MESSAGE = "<html>The shared place is used in one or more components.<br/>TAPAAL will unshare all places under this name,<br/>but leave the places in the components.</html>";49 private static final String PLACE_IS_USED_MESSAGE = "<html>The shared place is used in one or more components.<br/>TAPAAL will unshare all places under this name,<br/>but leave the places in the components.</html>";
4850
@@ -203,10 +205,9 @@
203 int index = list.getSelectedIndex();205 int index = list.getSelectedIndex();
204 206
205 if(index > 0) {207 if(index > 0) {
206 if(isDisplayingTransitions())208 Command c = new MoveElementUpCommand(SharedPlacesAndTransitionsPanel.this, index, index-1);
207 sharedTransitionsListModel.swap(index, index-1);209 undoManager.addNewEdit(c);
208 else210 c.redo();
209 sharedPlacesListModel.swap(index, index-1);
210 list.setSelectedIndex(index-1);211 list.setSelectedIndex(index-1);
211 list.ensureIndexIsVisible(index-1);212 list.ensureIndexIsVisible(index-1);
212 }213 }
@@ -226,20 +227,11 @@
226 public void actionPerformed(ActionEvent e) {227 public void actionPerformed(ActionEvent e) {
227 int index = list.getSelectedIndex();228 int index = list.getSelectedIndex();
228 229
229 if(isDisplayingTransitions()) {230 Command c = new MoveElementDownCommand(SharedPlacesAndTransitionsPanel.this, index, index+1);
230 if(index < sharedTransitionsListModel.getSize() - 1) {231 undoManager.addNewEdit(c);
231 sharedTransitionsListModel.swap(index, index+1);232 c.redo();
232 list.setSelectedIndex(index+1);233 list.setSelectedIndex(index+1);
233 list.ensureIndexIsVisible(index+1);234 list.ensureIndexIsVisible(index+1);
234
235 }
236 } else {
237 if(index < sharedPlacesListModel.getSize() - 1) {
238 sharedPlacesListModel.swap(index, index+1);
239 list.setSelectedIndex(index+1);
240 list.ensureIndexIsVisible(index+1);
241 }
242 }
243 }235 }
244 });236 });
245 237
@@ -626,4 +618,30 @@
626 fireContentsChanged(this, 0, network.numberOfSharedTransitions());618 fireContentsChanged(this, 0, network.numberOfSharedTransitions());
627 }619 }
628 }620 }
621
622 @Override
623 public void moveUp(int index) {
624 if(isDisplayingTransitions())
625 sharedTransitionsListModel.swap(index, index-1);
626 else
627 sharedPlacesListModel.swap(index, index-1);
628 }
629
630 @Override
631 public void moveDown(int index) {
632 if(isDisplayingTransitions()) {
633 if(index < sharedTransitionsListModel.getSize() - 1) {
634 sharedTransitionsListModel.swap(index, index+1);
635 }
636 } else {
637 if(index < sharedPlacesListModel.getSize() - 1) {
638 sharedPlacesListModel.swap(index, index+1);
639 }
640 }
641 }
642
643 @Override
644 public JList getJList() {
645 return list;
646 }
629}647}
630648
=== modified file 'src/dk/aau/cs/gui/TemplateExplorer.java'
--- src/dk/aau/cs/gui/TemplateExplorer.java 2019-01-24 20:01:38 +0000
+++ src/dk/aau/cs/gui/TemplateExplorer.java 2020-05-16 08:49:46 +0000
@@ -59,6 +59,8 @@
59import dk.aau.cs.TCTL.visitors.ContainsPlaceWithDisabledTemplateVisitor;59import dk.aau.cs.TCTL.visitors.ContainsPlaceWithDisabledTemplateVisitor;
60import dk.aau.cs.gui.components.NonsearchableJList;60import dk.aau.cs.gui.components.NonsearchableJList;
61import dk.aau.cs.gui.undo.Command;61import dk.aau.cs.gui.undo.Command;
62import dk.aau.cs.gui.undo.MoveElementDownCommand;
63import dk.aau.cs.gui.undo.MoveElementUpCommand;
62import dk.aau.cs.gui.undo.SortTemplatesCommand;64import dk.aau.cs.gui.undo.SortTemplatesCommand;
63import dk.aau.cs.model.tapn.Constant;65import dk.aau.cs.model.tapn.Constant;
64import dk.aau.cs.model.tapn.SharedTransition;66import dk.aau.cs.model.tapn.SharedTransition;
@@ -68,8 +70,10 @@
68import dk.aau.cs.util.Require;70import dk.aau.cs.util.Require;
69import dk.aau.cs.util.StringComparator;71import dk.aau.cs.util.StringComparator;
70import dk.aau.cs.util.Tuple;72import dk.aau.cs.util.Tuple;
7173import pipe.gui.widgets.SidePane;
72public class TemplateExplorer extends JPanel {74
75
76public class TemplateExplorer extends JPanel implements SidePane{
73 private static final long serialVersionUID = -2334464984237161208L;77 private static final long serialVersionUID = -2334464984237161208L;
7478
75 // Template explorer panel items79 // Template explorer panel items
@@ -252,10 +256,9 @@
252 int index = templateList.getSelectedIndex();256 int index = templateList.getSelectedIndex();
253 257
254 if(index > 0) {258 if(index > 0) {
255 parent.swapTemplates(index, index-1);259 Command c = new MoveElementUpCommand(TemplateExplorer.this, index, index-1);
256 Object o = listModel.getElementAt(index);260 undoManager.addNewEdit(c);
257 listModel.setElementAt(listModel.getElementAt(index-1), index);261 c.redo();
258 listModel.setElementAt(o, index-1);
259 templateList.ensureIndexIsVisible(index+1);262 templateList.ensureIndexIsVisible(index+1);
260 templateList.setSelectedIndex(index-1);263 templateList.setSelectedIndex(index-1);
261 }264 }
@@ -276,10 +279,9 @@
276 int index = templateList.getSelectedIndex();279 int index = templateList.getSelectedIndex();
277 280
278 if(index < parent.network().allTemplates().size() - 1) {281 if(index < parent.network().allTemplates().size() - 1) {
279 parent.swapTemplates(index, index+1);282 Command c = new MoveElementDownCommand(TemplateExplorer.this, index, index+1);
280 Object o = listModel.getElementAt(index);283 undoManager.addNewEdit(c);
281 listModel.setElementAt(listModel.getElementAt(index+1), index);284 c.redo();
282 listModel.setElementAt(o, index+1);
283 templateList.ensureIndexIsVisible(index+1);285 templateList.ensureIndexIsVisible(index+1);
284 templateList.setSelectedIndex(index+1);286 templateList.setSelectedIndex(index+1);
285 }287 }
@@ -1031,4 +1033,23 @@
1031 }1033 }
1032 1034
1033 }1035 }
1036 @Override
1037 public void moveUp(int index) {
1038 parent.swapTemplates(index, index-1);
1039 Object o = listModel.getElementAt(index);
1040 listModel.setElementAt(listModel.getElementAt(index-1), index);
1041 listModel.setElementAt(o, index-1);
1042 }
1043
1044 @Override
1045 public void moveDown(int index) {
1046 parent.swapTemplates(index, index+1);
1047 Object o = listModel.getElementAt(index);
1048 listModel.setElementAt(listModel.getElementAt(index+1), index);
1049 listModel.setElementAt(o, index+1);
1050 }
1051 @Override
1052 public JList getJList(){
1053 return templateList;
1054 }
1034}1055}
10351056
=== added file 'src/dk/aau/cs/gui/undo/MoveElementDownCommand.java'
--- src/dk/aau/cs/gui/undo/MoveElementDownCommand.java 1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/gui/undo/MoveElementDownCommand.java 2020-05-16 08:49:46 +0000
@@ -0,0 +1,46 @@
1package dk.aau.cs.gui.undo;
2
3import pipe.dataLayer.Template;
4import pipe.gui.widgets.SidePane;
5
6import javax.swing.*;
7
8public class MoveElementDownCommand extends Command{
9 int oldIndex;
10 int newIndex;
11 SidePane sidePane;
12 JList<Template> templateList;
13 public MoveElementDownCommand(SidePane sidePane, int oldIndex, int newIndex){
14 this.oldIndex = oldIndex;
15 this.newIndex = newIndex;
16 this.sidePane = sidePane;
17 }
18
19 @Override
20 public void redo() {
21 if(sidePane.getJList().getSelectedIndex() == oldIndex){
22 sidePane.moveDown(oldIndex);
23 sidePane.getJList().setSelectedIndex(oldIndex+1);
24 }else if(sidePane.getJList().getSelectedIndex() == oldIndex+1){
25 sidePane.moveDown(oldIndex);
26 sidePane.getJList().setSelectedIndex(newIndex-1);
27 } else{
28 sidePane.moveDown(oldIndex);
29 }
30 sidePane.getJList().updateUI();
31 }
32
33 @Override
34 public void undo() {
35 if(sidePane.getJList().getSelectedIndex() == newIndex){
36 sidePane.moveUp(newIndex);
37 sidePane.getJList().setSelectedIndex(newIndex-1);
38 } else if(sidePane.getJList().getSelectedIndex() == newIndex-1){
39 sidePane.moveUp(newIndex);
40 sidePane.getJList().setSelectedIndex(oldIndex+1);
41 }else{
42 sidePane.moveUp(newIndex);
43 }
44 sidePane.getJList().updateUI();
45 }
46}
047
=== added file 'src/dk/aau/cs/gui/undo/MoveElementUpCommand.java'
--- src/dk/aau/cs/gui/undo/MoveElementUpCommand.java 1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/gui/undo/MoveElementUpCommand.java 2020-05-16 08:49:46 +0000
@@ -0,0 +1,51 @@
1package dk.aau.cs.gui.undo;
2
3import pipe.dataLayer.Template;
4import pipe.gui.widgets.SidePane;
5
6import javax.swing.*;
7
8public class MoveElementUpCommand extends Command{
9 int oldIndex;
10 int newIndex;
11 SidePane sidePane;
12 JList<Template> templateList;
13 public MoveElementUpCommand(SidePane sidePane, int oldIndex, int newIndex){
14 this.oldIndex = oldIndex;
15 this.newIndex = newIndex;
16 this.sidePane = sidePane;
17 }
18
19 @Override
20 public void redo() {
21 if(sidePane.getJList().getSelectedIndex() == oldIndex){
22 sidePane.moveUp(oldIndex);
23 sidePane.getJList().setSelectedIndex(oldIndex-1);
24 sidePane.getJList().ensureIndexIsVisible(oldIndex-1);
25 } else if(sidePane.getJList().getSelectedIndex() == oldIndex-1){
26 sidePane.moveUp(oldIndex);
27 sidePane.getJList().setSelectedIndex(newIndex+1);
28 sidePane.getJList().ensureIndexIsVisible(newIndex+1);
29 }else{
30 sidePane.moveUp(oldIndex);
31 }
32 sidePane.getJList().updateUI();
33
34 }
35
36 @Override
37 public void undo() {
38 if(sidePane.getJList().getSelectedIndex() == newIndex){
39 sidePane.moveDown(newIndex);
40 sidePane.getJList().setSelectedIndex(newIndex+1);
41 sidePane.getJList().ensureIndexIsVisible(newIndex+1);
42 }else if(sidePane.getJList().getSelectedIndex() == newIndex+1){
43 sidePane.moveDown(newIndex);
44 sidePane.getJList().setSelectedIndex(oldIndex-1);
45 sidePane.getJList().ensureIndexIsVisible(oldIndex-1);
46 } else{
47 sidePane.moveDown(newIndex);
48 }
49 sidePane.getJList().updateUI();
50 }
51}
052
=== modified file 'src/pipe/gui/widgets/ConstantsPane.java'
--- src/pipe/gui/widgets/ConstantsPane.java 2020-01-12 12:27:45 +0000
+++ src/pipe/gui/widgets/ConstantsPane.java 2020-05-16 08:49:46 +0000
@@ -19,7 +19,6 @@
19import java.awt.event.MouseEvent;19import java.awt.event.MouseEvent;
20import java.io.IOException;20import java.io.IOException;
2121
22
23import javax.swing.BorderFactory;22import javax.swing.BorderFactory;
24import javax.swing.ImageIcon;23import javax.swing.ImageIcon;
25import javax.swing.JButton;24import javax.swing.JButton;
@@ -39,13 +38,15 @@
39import pipe.gui.CreateGui;38import pipe.gui.CreateGui;
40import dk.aau.cs.gui.TabContent;39import dk.aau.cs.gui.TabContent;
41import dk.aau.cs.gui.undo.Command;40import dk.aau.cs.gui.undo.Command;
41import dk.aau.cs.gui.undo.MoveElementDownCommand;
42import dk.aau.cs.gui.undo.MoveElementUpCommand;
42import dk.aau.cs.gui.undo.SortConstantsCommand;43import dk.aau.cs.gui.undo.SortConstantsCommand;
43import dk.aau.cs.model.tapn.Constant;44import dk.aau.cs.model.tapn.Constant;
44import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;45import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
45import dk.aau.cs.gui.components.ConstantsListModel;46import dk.aau.cs.gui.components.ConstantsListModel;
46import dk.aau.cs.gui.components.NonsearchableJList;47import dk.aau.cs.gui.components.NonsearchableJList;
4748
48public class ConstantsPane extends JPanel {49public class ConstantsPane extends JPanel implements SidePane {
49 private static final long serialVersionUID = -7883351020889779067L;50 private static final long serialVersionUID = -7883351020889779067L;
50 private JPanel constantsPanel;51 private JPanel constantsPanel;
51 private JScrollPane constantsScroller;52 private JScrollPane constantsScroller;
@@ -362,8 +363,9 @@
362 int index = constantsList.getSelectedIndex();363 int index = constantsList.getSelectedIndex();
363364
364 if(index > 0) {365 if(index > 0) {
365 parent.swapConstants(index, index-1);366 Command c = new MoveElementUpCommand(ConstantsPane.this, index, index-1);
366 showConstants();367 CreateGui.getDrawingSurface().getUndoManager().addNewEdit(c);
368 c.redo();
367 constantsList.setSelectedIndex(index-1);369 constantsList.setSelectedIndex(index-1);
368 }370 }
369 }371 }
@@ -383,8 +385,9 @@
383 int index = constantsList.getSelectedIndex();385 int index = constantsList.getSelectedIndex();
384386
385 if(index < parent.network().constants().size() - 1) {387 if(index < parent.network().constants().size() - 1) {
386 parent.swapConstants(index, index+1);388 Command c = new MoveElementDownCommand(ConstantsPane.this, index, index+1);
387 showConstants();389 CreateGui.getDrawingSurface().getUndoManager().addNewEdit(c);
390 c.redo();
388 constantsList.setSelectedIndex(index+1);391 constantsList.setSelectedIndex(index+1);
389 }392 }
390 }393 }
@@ -480,4 +483,21 @@
480 constantsList.setSelectedIndex(0);483 constantsList.setSelectedIndex(0);
481484
482 }485 }
486
487 @Override
488 public void moveUp(int index) {
489 parent.swapConstants(index, index-1);
490 showConstants();
491 }
492
493 @Override
494 public void moveDown(int index) {
495 parent.swapConstants(index, index+1);
496 showConstants();
497 }
498
499 @Override
500 public JList getJList() {
501 return constantsList;
502 }
483}503}
484504
=== modified file 'src/pipe/gui/widgets/QueryPane.java'
--- src/pipe/gui/widgets/QueryPane.java 2019-01-24 20:03:51 +0000
+++ src/pipe/gui/widgets/QueryPane.java 2020-05-16 08:49:46 +0000
@@ -42,12 +42,14 @@
42import dk.aau.cs.gui.BatchProcessingDialog;42import dk.aau.cs.gui.BatchProcessingDialog;
43import dk.aau.cs.gui.TabContent;43import dk.aau.cs.gui.TabContent;
44import dk.aau.cs.gui.undo.Command;44import dk.aau.cs.gui.undo.Command;
45import dk.aau.cs.gui.undo.MoveElementDownCommand;
46import dk.aau.cs.gui.undo.MoveElementUpCommand;
45import dk.aau.cs.gui.undo.SortQueriesCommand;47import dk.aau.cs.gui.undo.SortQueriesCommand;
46import dk.aau.cs.gui.components.NonsearchableJList;48import dk.aau.cs.gui.components.NonsearchableJList;
47import dk.aau.cs.translations.ReductionOption;49import dk.aau.cs.translations.ReductionOption;
48import dk.aau.cs.util.Require;50import dk.aau.cs.util.Require;
4951
50public class QueryPane extends JPanel {52public class QueryPane extends JPanel implements SidePane {
51 private static final long serialVersionUID = 4062539545170994654L;53 private static final long serialVersionUID = 4062539545170994654L;
52 private JPanel queryCollectionPanel;54 private JPanel queryCollectionPanel;
53 private JPanel buttonsPanel;55 private JPanel buttonsPanel;
@@ -216,7 +218,9 @@
216 int index = queryList.getSelectedIndex();218 int index = queryList.getSelectedIndex();
217219
218 if(index > 0 && queryList.getSelectedIndices().length == 1) {220 if(index > 0 && queryList.getSelectedIndices().length == 1) {
219 swapQueries(index, index-1);221 Command c = new MoveElementUpCommand(QueryPane.this, index, index-1);
222 undoManager.addNewEdit(c);
223 c.redo();
220 queryList.setSelectedIndex(index-1);224 queryList.setSelectedIndex(index-1);
221 }225 }
222 else226 else
@@ -238,8 +242,10 @@
238 int index = queryList.getSelectedIndex();242 int index = queryList.getSelectedIndex();
239243
240 if(index < listModel.size()-1 && queryList.getSelectedIndices().length == 1) {244 if(index < listModel.size()-1 && queryList.getSelectedIndices().length == 1) {
241 swapQueries(index, index+1);245 Command c = new MoveElementDownCommand(QueryPane.this, index, index+1);
242 queryList.setSelectedIndex(index+1);246 undoManager.addNewEdit(c);
247 c.redo();
248 queryList.setSelectedIndex(index+1);
243 }249 }
244 else250 else
245 moveDownButton.setEnabled(false);251 moveDownButton.setEnabled(false);
@@ -527,4 +533,17 @@
527 public void verifySelectedQuery() {533 public void verifySelectedQuery() {
528 verifyQuery();534 verifyQuery();
529 }535 }
536
537 @Override
538 public void moveUp(int index){
539 swapQueries(index, index-1);
540 }
541 @Override
542 public void moveDown(int index){
543 swapQueries(index, index+1);
544 }
545 @Override
546 public JList getJList(){
547 return queryList;
548 }
530}549}
531550
=== added file 'src/pipe/gui/widgets/SidePane.java'
--- src/pipe/gui/widgets/SidePane.java 1970-01-01 00:00:00 +0000
+++ src/pipe/gui/widgets/SidePane.java 2020-05-16 08:49:46 +0000
@@ -0,0 +1,9 @@
1package pipe.gui.widgets;
2
3import javax.swing.*;
4
5public interface SidePane {
6 public void moveUp(int index);
7 public void moveDown(int index);
8 public JList getJList();
9}

Subscribers

People subscribed via source and target branches