Merge lp:~tapaal-contributor/tapaal/undo-up-down-sidepane-3.6-1870894 into lp:tapaal/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
1=== modified file 'src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java'
2--- src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2019-03-02 11:14:31 +0000
3+++ src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2020-05-16 08:49:46 +0000
4@@ -30,10 +30,12 @@
5 import pipe.gui.CreateGui;
6 import pipe.gui.undo.UndoManager;
7 import pipe.gui.widgets.EscapableDialog;
8-
9+import pipe.gui.widgets.SidePane;
10 import dk.aau.cs.gui.components.NonsearchableJList;
11 import dk.aau.cs.gui.undo.AddSharedPlaceCommand;
12 import dk.aau.cs.gui.undo.Command;
13+import dk.aau.cs.gui.undo.MoveElementDownCommand;
14+import dk.aau.cs.gui.undo.MoveElementUpCommand;
15 import dk.aau.cs.gui.undo.SortSharedPlacesCommand;
16 import dk.aau.cs.gui.undo.SortSharedTransitionsCommand;
17 import dk.aau.cs.model.tapn.SharedPlace;
18@@ -42,7 +44,7 @@
19 import dk.aau.cs.util.Require;
20 import dk.aau.cs.util.RequireException;
21
22-public class SharedPlacesAndTransitionsPanel extends JPanel {
23+public class SharedPlacesAndTransitionsPanel extends JPanel implements SidePane{
24 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>";
25 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>";
26
27@@ -203,10 +205,9 @@
28 int index = list.getSelectedIndex();
29
30 if(index > 0) {
31- if(isDisplayingTransitions())
32- sharedTransitionsListModel.swap(index, index-1);
33- else
34- sharedPlacesListModel.swap(index, index-1);
35+ Command c = new MoveElementUpCommand(SharedPlacesAndTransitionsPanel.this, index, index-1);
36+ undoManager.addNewEdit(c);
37+ c.redo();
38 list.setSelectedIndex(index-1);
39 list.ensureIndexIsVisible(index-1);
40 }
41@@ -226,20 +227,11 @@
42 public void actionPerformed(ActionEvent e) {
43 int index = list.getSelectedIndex();
44
45- if(isDisplayingTransitions()) {
46- if(index < sharedTransitionsListModel.getSize() - 1) {
47- sharedTransitionsListModel.swap(index, index+1);
48- list.setSelectedIndex(index+1);
49- list.ensureIndexIsVisible(index+1);
50-
51- }
52- } else {
53- if(index < sharedPlacesListModel.getSize() - 1) {
54- sharedPlacesListModel.swap(index, index+1);
55- list.setSelectedIndex(index+1);
56- list.ensureIndexIsVisible(index+1);
57- }
58- }
59+ Command c = new MoveElementDownCommand(SharedPlacesAndTransitionsPanel.this, index, index+1);
60+ undoManager.addNewEdit(c);
61+ c.redo();
62+ list.setSelectedIndex(index+1);
63+ list.ensureIndexIsVisible(index+1);
64 }
65 });
66
67@@ -626,4 +618,30 @@
68 fireContentsChanged(this, 0, network.numberOfSharedTransitions());
69 }
70 }
71+
72+ @Override
73+ public void moveUp(int index) {
74+ if(isDisplayingTransitions())
75+ sharedTransitionsListModel.swap(index, index-1);
76+ else
77+ sharedPlacesListModel.swap(index, index-1);
78+ }
79+
80+ @Override
81+ public void moveDown(int index) {
82+ if(isDisplayingTransitions()) {
83+ if(index < sharedTransitionsListModel.getSize() - 1) {
84+ sharedTransitionsListModel.swap(index, index+1);
85+ }
86+ } else {
87+ if(index < sharedPlacesListModel.getSize() - 1) {
88+ sharedPlacesListModel.swap(index, index+1);
89+ }
90+ }
91+ }
92+
93+ @Override
94+ public JList getJList() {
95+ return list;
96+ }
97 }
98
99=== modified file 'src/dk/aau/cs/gui/TemplateExplorer.java'
100--- src/dk/aau/cs/gui/TemplateExplorer.java 2019-01-24 20:01:38 +0000
101+++ src/dk/aau/cs/gui/TemplateExplorer.java 2020-05-16 08:49:46 +0000
102@@ -59,6 +59,8 @@
103 import dk.aau.cs.TCTL.visitors.ContainsPlaceWithDisabledTemplateVisitor;
104 import dk.aau.cs.gui.components.NonsearchableJList;
105 import dk.aau.cs.gui.undo.Command;
106+import dk.aau.cs.gui.undo.MoveElementDownCommand;
107+import dk.aau.cs.gui.undo.MoveElementUpCommand;
108 import dk.aau.cs.gui.undo.SortTemplatesCommand;
109 import dk.aau.cs.model.tapn.Constant;
110 import dk.aau.cs.model.tapn.SharedTransition;
111@@ -68,8 +70,10 @@
112 import dk.aau.cs.util.Require;
113 import dk.aau.cs.util.StringComparator;
114 import dk.aau.cs.util.Tuple;
115-
116-public class TemplateExplorer extends JPanel {
117+import pipe.gui.widgets.SidePane;
118+
119+
120+public class TemplateExplorer extends JPanel implements SidePane{
121 private static final long serialVersionUID = -2334464984237161208L;
122
123 // Template explorer panel items
124@@ -252,10 +256,9 @@
125 int index = templateList.getSelectedIndex();
126
127 if(index > 0) {
128- parent.swapTemplates(index, index-1);
129- Object o = listModel.getElementAt(index);
130- listModel.setElementAt(listModel.getElementAt(index-1), index);
131- listModel.setElementAt(o, index-1);
132+ Command c = new MoveElementUpCommand(TemplateExplorer.this, index, index-1);
133+ undoManager.addNewEdit(c);
134+ c.redo();
135 templateList.ensureIndexIsVisible(index+1);
136 templateList.setSelectedIndex(index-1);
137 }
138@@ -276,10 +279,9 @@
139 int index = templateList.getSelectedIndex();
140
141 if(index < parent.network().allTemplates().size() - 1) {
142- parent.swapTemplates(index, index+1);
143- Object o = listModel.getElementAt(index);
144- listModel.setElementAt(listModel.getElementAt(index+1), index);
145- listModel.setElementAt(o, index+1);
146+ Command c = new MoveElementDownCommand(TemplateExplorer.this, index, index+1);
147+ undoManager.addNewEdit(c);
148+ c.redo();
149 templateList.ensureIndexIsVisible(index+1);
150 templateList.setSelectedIndex(index+1);
151 }
152@@ -1031,4 +1033,23 @@
153 }
154
155 }
156+ @Override
157+ public void moveUp(int index) {
158+ parent.swapTemplates(index, index-1);
159+ Object o = listModel.getElementAt(index);
160+ listModel.setElementAt(listModel.getElementAt(index-1), index);
161+ listModel.setElementAt(o, index-1);
162+ }
163+
164+ @Override
165+ public void moveDown(int index) {
166+ parent.swapTemplates(index, index+1);
167+ Object o = listModel.getElementAt(index);
168+ listModel.setElementAt(listModel.getElementAt(index+1), index);
169+ listModel.setElementAt(o, index+1);
170+ }
171+ @Override
172+ public JList getJList(){
173+ return templateList;
174+ }
175 }
176
177=== added file 'src/dk/aau/cs/gui/undo/MoveElementDownCommand.java'
178--- src/dk/aau/cs/gui/undo/MoveElementDownCommand.java 1970-01-01 00:00:00 +0000
179+++ src/dk/aau/cs/gui/undo/MoveElementDownCommand.java 2020-05-16 08:49:46 +0000
180@@ -0,0 +1,46 @@
181+package dk.aau.cs.gui.undo;
182+
183+import pipe.dataLayer.Template;
184+import pipe.gui.widgets.SidePane;
185+
186+import javax.swing.*;
187+
188+public class MoveElementDownCommand extends Command{
189+ int oldIndex;
190+ int newIndex;
191+ SidePane sidePane;
192+ JList<Template> templateList;
193+ public MoveElementDownCommand(SidePane sidePane, int oldIndex, int newIndex){
194+ this.oldIndex = oldIndex;
195+ this.newIndex = newIndex;
196+ this.sidePane = sidePane;
197+ }
198+
199+ @Override
200+ public void redo() {
201+ if(sidePane.getJList().getSelectedIndex() == oldIndex){
202+ sidePane.moveDown(oldIndex);
203+ sidePane.getJList().setSelectedIndex(oldIndex+1);
204+ }else if(sidePane.getJList().getSelectedIndex() == oldIndex+1){
205+ sidePane.moveDown(oldIndex);
206+ sidePane.getJList().setSelectedIndex(newIndex-1);
207+ } else{
208+ sidePane.moveDown(oldIndex);
209+ }
210+ sidePane.getJList().updateUI();
211+ }
212+
213+ @Override
214+ public void undo() {
215+ if(sidePane.getJList().getSelectedIndex() == newIndex){
216+ sidePane.moveUp(newIndex);
217+ sidePane.getJList().setSelectedIndex(newIndex-1);
218+ } else if(sidePane.getJList().getSelectedIndex() == newIndex-1){
219+ sidePane.moveUp(newIndex);
220+ sidePane.getJList().setSelectedIndex(oldIndex+1);
221+ }else{
222+ sidePane.moveUp(newIndex);
223+ }
224+ sidePane.getJList().updateUI();
225+ }
226+}
227
228=== added file 'src/dk/aau/cs/gui/undo/MoveElementUpCommand.java'
229--- src/dk/aau/cs/gui/undo/MoveElementUpCommand.java 1970-01-01 00:00:00 +0000
230+++ src/dk/aau/cs/gui/undo/MoveElementUpCommand.java 2020-05-16 08:49:46 +0000
231@@ -0,0 +1,51 @@
232+package dk.aau.cs.gui.undo;
233+
234+import pipe.dataLayer.Template;
235+import pipe.gui.widgets.SidePane;
236+
237+import javax.swing.*;
238+
239+public class MoveElementUpCommand extends Command{
240+ int oldIndex;
241+ int newIndex;
242+ SidePane sidePane;
243+ JList<Template> templateList;
244+ public MoveElementUpCommand(SidePane sidePane, int oldIndex, int newIndex){
245+ this.oldIndex = oldIndex;
246+ this.newIndex = newIndex;
247+ this.sidePane = sidePane;
248+ }
249+
250+ @Override
251+ public void redo() {
252+ if(sidePane.getJList().getSelectedIndex() == oldIndex){
253+ sidePane.moveUp(oldIndex);
254+ sidePane.getJList().setSelectedIndex(oldIndex-1);
255+ sidePane.getJList().ensureIndexIsVisible(oldIndex-1);
256+ } else if(sidePane.getJList().getSelectedIndex() == oldIndex-1){
257+ sidePane.moveUp(oldIndex);
258+ sidePane.getJList().setSelectedIndex(newIndex+1);
259+ sidePane.getJList().ensureIndexIsVisible(newIndex+1);
260+ }else{
261+ sidePane.moveUp(oldIndex);
262+ }
263+ sidePane.getJList().updateUI();
264+
265+ }
266+
267+ @Override
268+ public void undo() {
269+ if(sidePane.getJList().getSelectedIndex() == newIndex){
270+ sidePane.moveDown(newIndex);
271+ sidePane.getJList().setSelectedIndex(newIndex+1);
272+ sidePane.getJList().ensureIndexIsVisible(newIndex+1);
273+ }else if(sidePane.getJList().getSelectedIndex() == newIndex+1){
274+ sidePane.moveDown(newIndex);
275+ sidePane.getJList().setSelectedIndex(oldIndex-1);
276+ sidePane.getJList().ensureIndexIsVisible(oldIndex-1);
277+ } else{
278+ sidePane.moveDown(newIndex);
279+ }
280+ sidePane.getJList().updateUI();
281+ }
282+}
283
284=== modified file 'src/pipe/gui/widgets/ConstantsPane.java'
285--- src/pipe/gui/widgets/ConstantsPane.java 2020-01-12 12:27:45 +0000
286+++ src/pipe/gui/widgets/ConstantsPane.java 2020-05-16 08:49:46 +0000
287@@ -19,7 +19,6 @@
288 import java.awt.event.MouseEvent;
289 import java.io.IOException;
290
291-
292 import javax.swing.BorderFactory;
293 import javax.swing.ImageIcon;
294 import javax.swing.JButton;
295@@ -39,13 +38,15 @@
296 import pipe.gui.CreateGui;
297 import dk.aau.cs.gui.TabContent;
298 import dk.aau.cs.gui.undo.Command;
299+import dk.aau.cs.gui.undo.MoveElementDownCommand;
300+import dk.aau.cs.gui.undo.MoveElementUpCommand;
301 import dk.aau.cs.gui.undo.SortConstantsCommand;
302 import dk.aau.cs.model.tapn.Constant;
303 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
304 import dk.aau.cs.gui.components.ConstantsListModel;
305 import dk.aau.cs.gui.components.NonsearchableJList;
306
307-public class ConstantsPane extends JPanel {
308+public class ConstantsPane extends JPanel implements SidePane {
309 private static final long serialVersionUID = -7883351020889779067L;
310 private JPanel constantsPanel;
311 private JScrollPane constantsScroller;
312@@ -362,8 +363,9 @@
313 int index = constantsList.getSelectedIndex();
314
315 if(index > 0) {
316- parent.swapConstants(index, index-1);
317- showConstants();
318+ Command c = new MoveElementUpCommand(ConstantsPane.this, index, index-1);
319+ CreateGui.getDrawingSurface().getUndoManager().addNewEdit(c);
320+ c.redo();
321 constantsList.setSelectedIndex(index-1);
322 }
323 }
324@@ -383,8 +385,9 @@
325 int index = constantsList.getSelectedIndex();
326
327 if(index < parent.network().constants().size() - 1) {
328- parent.swapConstants(index, index+1);
329- showConstants();
330+ Command c = new MoveElementDownCommand(ConstantsPane.this, index, index+1);
331+ CreateGui.getDrawingSurface().getUndoManager().addNewEdit(c);
332+ c.redo();
333 constantsList.setSelectedIndex(index+1);
334 }
335 }
336@@ -480,4 +483,21 @@
337 constantsList.setSelectedIndex(0);
338
339 }
340+
341+ @Override
342+ public void moveUp(int index) {
343+ parent.swapConstants(index, index-1);
344+ showConstants();
345+ }
346+
347+ @Override
348+ public void moveDown(int index) {
349+ parent.swapConstants(index, index+1);
350+ showConstants();
351+ }
352+
353+ @Override
354+ public JList getJList() {
355+ return constantsList;
356+ }
357 }
358
359=== modified file 'src/pipe/gui/widgets/QueryPane.java'
360--- src/pipe/gui/widgets/QueryPane.java 2019-01-24 20:03:51 +0000
361+++ src/pipe/gui/widgets/QueryPane.java 2020-05-16 08:49:46 +0000
362@@ -42,12 +42,14 @@
363 import dk.aau.cs.gui.BatchProcessingDialog;
364 import dk.aau.cs.gui.TabContent;
365 import dk.aau.cs.gui.undo.Command;
366+import dk.aau.cs.gui.undo.MoveElementDownCommand;
367+import dk.aau.cs.gui.undo.MoveElementUpCommand;
368 import dk.aau.cs.gui.undo.SortQueriesCommand;
369 import dk.aau.cs.gui.components.NonsearchableJList;
370 import dk.aau.cs.translations.ReductionOption;
371 import dk.aau.cs.util.Require;
372
373-public class QueryPane extends JPanel {
374+public class QueryPane extends JPanel implements SidePane {
375 private static final long serialVersionUID = 4062539545170994654L;
376 private JPanel queryCollectionPanel;
377 private JPanel buttonsPanel;
378@@ -216,7 +218,9 @@
379 int index = queryList.getSelectedIndex();
380
381 if(index > 0 && queryList.getSelectedIndices().length == 1) {
382- swapQueries(index, index-1);
383+ Command c = new MoveElementUpCommand(QueryPane.this, index, index-1);
384+ undoManager.addNewEdit(c);
385+ c.redo();
386 queryList.setSelectedIndex(index-1);
387 }
388 else
389@@ -238,8 +242,10 @@
390 int index = queryList.getSelectedIndex();
391
392 if(index < listModel.size()-1 && queryList.getSelectedIndices().length == 1) {
393- swapQueries(index, index+1);
394- queryList.setSelectedIndex(index+1);
395+ Command c = new MoveElementDownCommand(QueryPane.this, index, index+1);
396+ undoManager.addNewEdit(c);
397+ c.redo();
398+ queryList.setSelectedIndex(index+1);
399 }
400 else
401 moveDownButton.setEnabled(false);
402@@ -527,4 +533,17 @@
403 public void verifySelectedQuery() {
404 verifyQuery();
405 }
406+
407+ @Override
408+ public void moveUp(int index){
409+ swapQueries(index, index-1);
410+ }
411+ @Override
412+ public void moveDown(int index){
413+ swapQueries(index, index+1);
414+ }
415+ @Override
416+ public JList getJList(){
417+ return queryList;
418+ }
419 }
420
421=== added file 'src/pipe/gui/widgets/SidePane.java'
422--- src/pipe/gui/widgets/SidePane.java 1970-01-01 00:00:00 +0000
423+++ src/pipe/gui/widgets/SidePane.java 2020-05-16 08:49:46 +0000
424@@ -0,0 +1,9 @@
425+package pipe.gui.widgets;
426+
427+import javax.swing.*;
428+
429+public interface SidePane {
430+ public void moveUp(int index);
431+ public void moveDown(int index);
432+ public JList getJList();
433+}

Subscribers

People subscribed via source and target branches