Merge lp:~tapaal-contributor/tapaal/hide-show-names-1921393 into lp:tapaal

Proposed by Lena Ernstsen
Status: Superseded
Proposed branch: lp:~tapaal-contributor/tapaal/hide-show-names-1921393
Merge into: lp:tapaal
Diff against target: 747 lines (+437/-41)
14 files modified
src/dk/aau/cs/gui/TabContent.java (+59/-2)
src/dk/aau/cs/gui/TabContentActions.java (+7/-0)
src/dk/aau/cs/gui/components/NameVisibilityPanel.java (+247/-0)
src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java (+70/-0)
src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java (+2/-2)
src/pipe/gui/GuiFrame.java (+10/-4)
src/pipe/gui/GuiFrameActions.java (+1/-1)
src/pipe/gui/GuiFrameController.java (+0/-1)
src/pipe/gui/canvas/DrawingSurfaceImpl.java (+6/-4)
src/pipe/gui/graphicElements/PlaceTransitionObject.java (+2/-2)
src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+0/-1)
src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java (+0/-1)
src/pipe/gui/widgets/PlaceEditorPanel.java (+22/-23)
src/pipe/gui/widgets/TAPNTransitionEditor.java (+11/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/hide-show-names-1921393
Reviewer Review Type Date Requested Status
Jiri Srba Needs Fixing
Review via email: mp+406239@code.launchpad.net

This proposal supersedes a proposal from 2021-07-20.

This proposal has been superseded by a proposal from 2021-08-03.

Commit message

Visibility of all place/transition names can be changed through the view menu

Description of the change

Place/transition names stay hidden when opening new nets and when switching tabs and templates.

Go to the view menu and then press "Change visibility of transition/place names". This will open a dialog, where you choose which options you want. When pressing "ok", the changes will be executed.
When entering the dialog again, the dialog will remember the options selected last time it was closed.

It is also possible to undo/redo the change of visibility.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote : Posted in a previous version of this proposal

Open Intro example, select "hide place names" and the names disappear. Then click on the editing surface and the names appear again.

Also, select e.g. Place P2 and unclick in the dialog "Show place name". The disable showing place names and enable it again in the view menu. Showing the name for P2 should be still disabled. This should have a priority over "show place names" in the view menu (i.e. if explicitly disabled, it should not show the place names at all). The same for transitions.

To make the semantics more clear, perhaps rename the View items to "Hide place names" and "Hide transition names" and leave them initially unselected (i.g. a normal behaviour). When you select the "hide" menu option, all transition or place names should be hidden, once you deselect it again, it should return to normal behaviour (i.e. depending on the choice made in the place/transition editing dialog).

Also, when you open a new net, the View options for these two items should be set to default (showing the names).

review: Needs Fixing
Revision history for this message
Jiri Srba (srba) wrote (last edit ): Posted in a previous version of this proposal

The logics is broken. Run TAPAAL (notice that hide place/transitions names is set even though
it should not be), open a new net and go to view menu and click on "hide place names" which is now selected. Try to draw a new place and transition. The place has a name (even though it should not) and the transition does not have a name (even though it should).

review: Needs Fixing
Revision history for this message
Jiri Srba (srba) wrote :

Undo is broken: to reproduce open intro example, use the dialog to hide both place/transition names and then manually show the name of one selected place. Then try to undo and nothing happens (the selected place should be now without name).

review: Needs Fixing
1143. By Lena Ernstsen

Fixed undo/redo of single place/transition name visibility through editor panels

1144. By Lena Ernstsen

merged branch

1145. By Lena Ernstsen

Changed tooltip for 'Merge Composed Net'

1146. By Lena Ernstsen

Changed tooltip for 'Merge Composed Net'

Unmerged revisions

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/TabContent.java'
2--- src/dk/aau/cs/gui/TabContent.java 2020-10-30 21:14:42 +0000
3+++ src/dk/aau/cs/gui/TabContent.java 2021-08-03 08:52:27 +0000
4@@ -16,6 +16,7 @@
5 import dk.aau.cs.TCTL.*;
6 import dk.aau.cs.debug.Logger;
7 import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
8+import dk.aau.cs.gui.components.NameVisibilityPanel;
9 import dk.aau.cs.gui.components.StatisticsPanel;
10 import dk.aau.cs.gui.components.TransitionFireingComponent;
11 import dk.aau.cs.gui.undo.*;
12@@ -843,8 +844,14 @@
13
14 private WorkflowDialog workflowDialog = null;
15
16-
17- private TabContent(boolean isTimed, boolean isGame) {
18+ private NameVisibilityPanel nameVisibilityPanel = null;
19+
20+ private Boolean showNamesOption = null;
21+ private Boolean isSelectedComponentOption = null;
22+ private Boolean isPlaceOption = null;
23+ private Boolean isTransitionOption = null;
24+
25+ private TabContent(boolean isTimed, boolean isGame) {
26 this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(isTimed,isGame));
27 }
28
29@@ -903,6 +910,8 @@
30 this.setDividerSize(8);
31 //XXX must be after the animationcontroller is created
32 animationModeController = new CanvasAnimationController(getAnimator());
33+
34+ nameVisibilityPanel = new NameVisibilityPanel(this);
35 }
36
37 public TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) {
38@@ -1621,6 +1630,39 @@
39 }
40 }
41
42+ @Override
43+ public Map<PetriNetObject, Boolean> showNames(boolean showNames, boolean placeNames, boolean selectedComponent) {
44+ Map<PetriNetObject, Boolean> map = new HashMap<>();
45+ List<PetriNetObject> components = new ArrayList<>();
46+
47+ if (selectedComponent) {
48+ Template template = currentTemplate();
49+ template.guiModel().getPetriNetObjects().forEach(components::add);
50+ } else {
51+ Iterable<Template> templates = allTemplates();
52+ for (Template template : templates) {
53+ template.guiModel().getPetriNetObjects().forEach(components::add);
54+ }
55+ }
56+
57+ for (Component component : components) {
58+ if (placeNames && component instanceof TimedPlaceComponent) {
59+ TimedPlaceComponent place = (TimedPlaceComponent) component;
60+ map.put(place, place.getAttributesVisible());
61+ place.setAttributesVisible(showNames);
62+ place.update(true);
63+ repaint();
64+ } else if (!placeNames && component instanceof TimedTransitionComponent) {
65+ TimedTransitionComponent transition = (TimedTransitionComponent) component;
66+ map.put(transition, transition.getAttributesVisible());
67+ transition.setAttributesVisible(showNames);
68+ transition.update(true);
69+ repaint();
70+ }
71+ }
72+ return map;
73+ }
74+
75 public static Split getEditorModelRoot(){
76 return editorModelroot;
77 }
78@@ -1839,6 +1881,21 @@
79 StatisticsPanel.showStatisticsPanel(drawingSurface().getModel().getStatistics());
80 }
81
82+ @Override
83+ public void showChangeNameVisibility() {
84+ NameVisibilityPanel panel = new NameVisibilityPanel(this);
85+ if (showNamesOption != null && isSelectedComponentOption != null && isPlaceOption != null && isTransitionOption != null) {
86+ panel.showNameVisibilityPanel(showNamesOption, isPlaceOption, isTransitionOption, isSelectedComponentOption);
87+ } else {
88+ panel.showNameVisibilityPanel();
89+ }
90+
91+ showNamesOption = panel.isShowNamesOption();
92+ isPlaceOption = panel.isPlaceOption();
93+ isTransitionOption = panel.isTransitionOption();
94+ isSelectedComponentOption = panel.isSelectedComponentOption();
95+ }
96+
97 @Override
98 public void importSUMOQueries() {
99 File[] files = FileBrowser.constructor("Import SUMO", "txt", FileBrowser.userPath).openFiles();
100
101=== modified file 'src/dk/aau/cs/gui/TabContentActions.java'
102--- src/dk/aau/cs/gui/TabContentActions.java 2020-08-11 11:51:55 +0000
103+++ src/dk/aau/cs/gui/TabContentActions.java 2021-08-03 08:52:27 +0000
104@@ -4,8 +4,10 @@
105 import pipe.gui.GuiFrameActions;
106 import pipe.gui.Pipe;
107 import pipe.gui.SafeGuiFrameActions;
108+import pipe.gui.graphicElements.PetriNetObject;
109
110 import java.io.File;
111+import java.util.Map;
112
113 public interface TabContentActions {
114
115@@ -96,4 +98,9 @@
116
117 void changeGameFeature(boolean isGame);
118
119+ Map<PetriNetObject, Boolean> showNames(boolean isVisible, boolean placeNames, boolean selectedComponent);
120+
121+ void showChangeNameVisibility();
122+
123+
124 }
125
126=== added file 'src/dk/aau/cs/gui/components/NameVisibilityPanel.java'
127--- src/dk/aau/cs/gui/components/NameVisibilityPanel.java 1970-01-01 00:00:00 +0000
128+++ src/dk/aau/cs/gui/components/NameVisibilityPanel.java 2021-08-03 08:52:27 +0000
129@@ -0,0 +1,247 @@
130+package dk.aau.cs.gui.components;
131+
132+import dk.aau.cs.gui.TabContent;
133+import dk.aau.cs.gui.undo.ChangeAllNamesVisibilityCommand;
134+import dk.aau.cs.gui.undo.Command;
135+import pipe.gui.graphicElements.PetriNetObject;
136+
137+import javax.swing.*;
138+import java.awt.*;
139+import java.util.HashMap;
140+import java.util.Map;
141+
142+public class NameVisibilityPanel extends JPanel {
143+ private static final String DIALOG_TITLE = "Change Name Visibility";
144+
145+ private static JDialog dialog;
146+ private JRadioButton showNames;
147+ private JRadioButton hideNames;
148+ private JRadioButton placeOption;
149+ private JRadioButton transitionOption;
150+ private JRadioButton bothOption;
151+ private JRadioButton selectedComponent;
152+ private JRadioButton allComponents;
153+
154+ ButtonGroup visibilityRadioButtonGroup;
155+ ButtonGroup objectRadioButtonGroup;
156+ ButtonGroup componentRadioButtonGroup;
157+
158+ JPanel visibilityPanel;
159+ JPanel placeTransitionPanel;
160+ JPanel componentPanel;
161+
162+ private final TabContent tab;
163+
164+ public NameVisibilityPanel(TabContent tab) {
165+ super(new GridBagLayout());
166+
167+ this.tab = tab;
168+
169+ init();
170+ }
171+
172+ public void showNameVisibilityPanel() {
173+ JOptionPane optionPane = new JOptionPane(this, JOptionPane.INFORMATION_MESSAGE);
174+
175+ dialog = optionPane.createDialog(DIALOG_TITLE);
176+ dialog.pack();
177+ dialog.setVisible(true);
178+
179+ Object selectedValue = optionPane.getValue();
180+
181+ if (selectedValue != null) ChangeNameVisibilityBasedOnSelection();
182+ }
183+
184+ public void showNameVisibilityPanel(boolean isVisible, boolean isPlace, boolean isTransition, boolean isSelectedComponent) {
185+ JOptionPane optionPane = new JOptionPane(this, JOptionPane.INFORMATION_MESSAGE);
186+
187+ showNames.setSelected(isVisible);
188+ hideNames.setSelected(!isVisible);
189+ placeOption.setSelected(isPlace && !isTransition);
190+ transitionOption.setSelected(isTransition && !isPlace);
191+ bothOption.setSelected(isPlace && isTransition);
192+ selectedComponent.setSelected(isSelectedComponent);
193+ allComponents.setSelected(!isSelectedComponent);
194+
195+ dialog = optionPane.createDialog(DIALOG_TITLE);
196+ dialog.pack();
197+ dialog.setVisible(true);
198+
199+ Object selectedValue = optionPane.getValue();
200+
201+ if (selectedValue != null) ChangeNameVisibilityBasedOnSelection();
202+ }
203+
204+ private void init() {
205+ visibilityPanel = initVisibilityOptions();
206+ placeTransitionPanel = initPlaceTransitionOptions();
207+ componentPanel = initComponentOptions();
208+
209+ GridBagConstraints gbc = new GridBagConstraints();
210+ gbc.gridx = 0;
211+ gbc.gridy = 0;
212+ gbc.anchor = GridBagConstraints.WEST;
213+ gbc.gridwidth = 3;
214+ gbc.insets = new Insets(5, 5, 5, 5);
215+
216+ this.add(visibilityPanel, gbc);
217+ gbc.gridy = 1;
218+ this.add(placeTransitionPanel, gbc);
219+ gbc.gridy = 2;
220+ this.add(componentPanel, gbc);
221+
222+ this.setVisible(true);
223+ }
224+
225+ private JPanel initVisibilityOptions() {
226+ JPanel panel = new JPanel(new GridBagLayout());
227+ visibilityRadioButtonGroup = new ButtonGroup();
228+
229+ JLabel text = new JLabel("Choose visibility: ");
230+ GridBagConstraints gbc = new GridBagConstraints();
231+ gbc.gridx = 0;
232+ gbc.gridy = 0;
233+ gbc.weightx = 0;
234+ gbc.anchor = GridBagConstraints.WEST;
235+ gbc.insets = new Insets(3, 3, 3, 3);
236+ panel.add(text, gbc);
237+
238+ showNames = new JRadioButton("Show");
239+ showNames.setSelected(true);
240+ gbc = new GridBagConstraints();
241+ gbc.gridx = 1;
242+ gbc.gridy = 0;
243+ gbc.weightx = 0;
244+ gbc.anchor = GridBagConstraints.WEST;
245+ gbc.insets = new Insets(3, 3, 3, 3);
246+ panel.add(showNames, gbc);
247+ visibilityRadioButtonGroup.add(showNames);
248+
249+ hideNames = new JRadioButton("Hide");
250+ gbc = new GridBagConstraints();
251+ gbc.gridx = 2;
252+ gbc.gridy = 0;
253+ gbc.weightx = 0;
254+ gbc.anchor = GridBagConstraints.WEST;
255+ gbc.insets = new Insets(3, 3, 3, 3);
256+ panel.add(hideNames, gbc);
257+ visibilityRadioButtonGroup.add(hideNames);
258+
259+ return panel;
260+ }
261+
262+ private JPanel initPlaceTransitionOptions() {
263+ JPanel panel = new JPanel(new GridBagLayout());
264+ objectRadioButtonGroup = new ButtonGroup();
265+
266+ JLabel text = new JLabel("Choose group: ");
267+ GridBagConstraints gbc = new GridBagConstraints();
268+ gbc.gridx = 0;
269+ gbc.gridy = 0;
270+ gbc.weightx = 0;
271+ gbc.anchor = GridBagConstraints.WEST;
272+ gbc.insets = new Insets(3, 3, 3, 3);
273+ panel.add(text, gbc);
274+
275+ placeOption = new JRadioButton("Places");
276+ placeOption.setSelected(true);
277+ gbc = new GridBagConstraints();
278+ gbc.gridx = 1;
279+ gbc.gridy = 0;
280+ gbc.weightx = 0;
281+ gbc.anchor = GridBagConstraints.WEST;
282+ gbc.insets = new Insets(3, 3, 3, 3);
283+ panel.add(placeOption, gbc);
284+ objectRadioButtonGroup.add(placeOption);
285+
286+ transitionOption = new JRadioButton("Transitions");
287+ gbc = new GridBagConstraints();
288+ gbc.gridx = 2;
289+ gbc.gridy = 0;
290+ gbc.weightx = 0;
291+ gbc.anchor = GridBagConstraints.WEST;
292+ gbc.insets = new Insets(3, 3, 3, 3);
293+ panel.add(transitionOption, gbc);
294+ objectRadioButtonGroup.add(transitionOption);
295+
296+ bothOption = new JRadioButton("Both");
297+ gbc = new GridBagConstraints();
298+ gbc.gridx = 3;
299+ gbc.gridy = 0;
300+ gbc.weightx = 0;
301+ gbc.anchor = GridBagConstraints.WEST;
302+ gbc.insets = new Insets(3, 3, 3, 3);
303+ panel.add(bothOption, gbc);
304+ objectRadioButtonGroup.add(bothOption);
305+
306+ return panel;
307+ }
308+
309+ private JPanel initComponentOptions() {
310+ JPanel panel = new JPanel(new GridBagLayout());
311+ componentRadioButtonGroup = new ButtonGroup();
312+
313+ JLabel text = new JLabel("Choose components: ");
314+ GridBagConstraints gbc = new GridBagConstraints();
315+ gbc.gridx = 0;
316+ gbc.gridy = 0;
317+ gbc.weightx = 0;
318+ gbc.anchor = GridBagConstraints.WEST;
319+ gbc.insets = new Insets(3, 3, 3, 3);
320+ panel.add(text, gbc);
321+
322+ selectedComponent = new JRadioButton("Selected component");
323+ selectedComponent.setSelected(true);
324+ gbc = new GridBagConstraints();
325+ gbc.gridx = 1;
326+ gbc.gridy = 0;
327+ gbc.weightx = 0;
328+ gbc.anchor = GridBagConstraints.WEST;
329+ gbc.insets = new Insets(3, 3, 3, 3);
330+ panel.add(selectedComponent, gbc);
331+ componentRadioButtonGroup.add(selectedComponent);
332+
333+ allComponents = new JRadioButton("All components");
334+ gbc = new GridBagConstraints();
335+ gbc.gridx = 2;
336+ gbc.gridy = 0;
337+ gbc.weightx = 0;
338+ gbc.anchor = GridBagConstraints.WEST;
339+ gbc.insets = new Insets(3, 3, 3, 3);
340+ panel.add(allComponents, gbc);
341+ componentRadioButtonGroup.add(allComponents);
342+
343+ return panel;
344+ }
345+
346+ protected void ChangeNameVisibilityBasedOnSelection() {
347+ Map<PetriNetObject, Boolean> places = new HashMap<>();
348+ Map<PetriNetObject, Boolean> transitions = new HashMap<>();
349+
350+ if (placeOption.isSelected() || bothOption.isSelected()) {
351+ places = tab.showNames(showNames.isSelected(), true, selectedComponent.isSelected());
352+ }
353+ if (transitionOption.isSelected() || bothOption.isSelected()) {
354+ transitions = tab.showNames(showNames.isSelected(), false, selectedComponent.isSelected());
355+ }
356+
357+ Command changeVisibilityCommand = new ChangeAllNamesVisibilityCommand(tab, places, transitions, showNames.isSelected());
358+ tab.getUndoManager().addNewEdit(changeVisibilityCommand);
359+ }
360+
361+ public boolean isShowNamesOption() {
362+ return showNames.isSelected();
363+ }
364+
365+ public boolean isSelectedComponentOption() {
366+ return selectedComponent.isSelected();
367+ }
368+
369+ public boolean isPlaceOption() {
370+ return placeOption.isSelected() || bothOption.isSelected();
371+ }
372+
373+ public boolean isTransitionOption() {
374+ return transitionOption.isSelected() || bothOption.isSelected();
375+ }
376+}
377
378=== added file 'src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java'
379--- src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java 1970-01-01 00:00:00 +0000
380+++ src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java 2021-08-03 08:52:27 +0000
381@@ -0,0 +1,70 @@
382+package dk.aau.cs.gui.undo;
383+
384+import dk.aau.cs.gui.TabContent;
385+import pipe.gui.graphicElements.PetriNetObject;
386+import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
387+import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
388+
389+import java.util.Map;
390+
391+public class ChangeAllNamesVisibilityCommand extends Command {
392+ private final Map<PetriNetObject, Boolean> places;
393+ private final Map<PetriNetObject, Boolean> transitions;
394+ private final boolean isVisible;
395+ private final TabContent tabContent;
396+
397+ public ChangeAllNamesVisibilityCommand(TabContent tabContent, Map<PetriNetObject, Boolean> places, Map<PetriNetObject, Boolean> transitions, boolean isVisible) {
398+ this.tabContent = tabContent;
399+ this.places = places;
400+ this.transitions= transitions;
401+ this.isVisible = isVisible;
402+ }
403+
404+ @Override
405+ public void redo() {
406+ if (places != null) {
407+ for (PetriNetObject place : places.keySet()) {
408+ if (place instanceof TimedPlaceComponent) {
409+ TimedPlaceComponent component = (TimedPlaceComponent) place;
410+ component.setAttributesVisible(isVisible);
411+ component.update(true);
412+ tabContent.repaint();
413+ }
414+ }
415+ }
416+ if (transitions != null) {
417+ for (PetriNetObject transition : transitions.keySet()) {
418+ if (transition instanceof TimedTransitionComponent) {
419+ TimedTransitionComponent component = (TimedTransitionComponent) transition;
420+ component.setAttributesVisible(isVisible);
421+ component.update(true);
422+ tabContent.repaint();
423+ }
424+ }
425+ }
426+ }
427+
428+ @Override
429+ public void undo() {
430+ if (places != null) {
431+ for (PetriNetObject place : places.keySet()) {
432+ if (place instanceof TimedPlaceComponent) {
433+ TimedPlaceComponent component = (TimedPlaceComponent) place;
434+ component.setAttributesVisible(places.get(component));
435+ component.update(true);
436+ tabContent.repaint();
437+ }
438+ }
439+ }
440+ if (transitions != null) {
441+ for (PetriNetObject transition : transitions.keySet()) {
442+ if (transition instanceof TimedTransitionComponent) {
443+ TimedTransitionComponent component = (TimedTransitionComponent) transition;
444+ component.setAttributesVisible(transitions.get(component));
445+ component.update(true);
446+ tabContent.repaint();
447+ }
448+ }
449+ }
450+ }
451+}
452
453=== modified file 'src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java'
454--- src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java 2011-03-12 12:12:12 +0000
455+++ src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java 2021-08-03 08:52:27 +0000
456@@ -22,13 +22,13 @@
457 public void redo() {
458 place.setName(newName);
459 updateQueries(oldName, newName);
460- }
461+ }
462
463 @Override
464 public void undo() {
465 place.setName(oldName);
466 updateQueries(newName,oldName);
467- }
468+ }
469
470 private void updateQueries(String nameToFind, String nameToInsert){
471 RenamePlaceTCTLVisitor renameVisitor = new RenamePlaceTCTLVisitor(nameToFind, nameToInsert);
472
473=== modified file 'src/pipe/gui/GuiFrame.java'
474--- src/pipe/gui/GuiFrame.java 2021-04-08 08:39:05 +0000
475+++ src/pipe/gui/GuiFrame.java 2021-08-03 08:52:27 +0000
476@@ -18,10 +18,8 @@
477
478 import com.sun.jna.Platform;
479 import dk.aau.cs.gui.*;
480-import dk.aau.cs.model.tapn.TimedArcPetriNet;
481 import dk.aau.cs.util.JavaUtil;
482 import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
483-import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter;
484 import net.tapaal.Preferences;
485 import net.tapaal.TAPAAL;
486 import net.tapaal.helpers.Reference.MutableReference;
487@@ -30,10 +28,8 @@
488 import net.tapaal.swinghelpers.SwingHelper;
489 import net.tapaal.swinghelpers.ToggleButtonWithoutText;
490 import org.jetbrains.annotations.NotNull;
491-import pipe.dataLayer.TAPNQuery;
492 import pipe.gui.Pipe.ElementType;
493 import pipe.gui.action.GuiAction;
494-import pipe.gui.widgets.WorkflowDialog;
495 import dk.aau.cs.debug.Logger;
496 import dk.aau.cs.gui.smartDraw.SmartDrawDialog;
497 import net.tapaal.resourcemanager.ResourceManager;
498@@ -334,6 +330,11 @@
499 guiFrameController.ifPresent(GuiFrameControllerActions::toggleDisplayToolTips);
500 }
501 };
502+ private final GuiAction changeNameVisibility = new GuiAction("Change visibility of transition/place names", "Executing this action will open a dialog where you can hide or show place and transition names", true) {
503+ public void actionPerformed(ActionEvent e) {
504+ currentTab.ifPresent(TabContentActions::showChangeNameVisibility);
505+ }
506+ };
507 private final GuiAction showAdvancedWorkspaceAction = new GuiAction("Show advanced workspace", "Show all panels", false) {
508 public void actionPerformed(ActionEvent e) {
509 guiFrameController.ifPresent(GuiFrameControllerActions::showAdvancedWorkspace);
510@@ -677,6 +678,10 @@
511
512 viewMenu.addSeparator();
513
514+ viewMenu.add(changeNameVisibility);
515+
516+ viewMenu.addSeparator();
517+
518 viewMenu.add(showSimpleWorkspaceAction);
519 viewMenu.add(showAdvancedWorkspaceAction);
520 viewMenu.add(saveWorkSpaceAction);
521@@ -1066,6 +1071,7 @@
522 showDelayEnabledTransitionsAction.setEnabled(enable);
523 showToolTipsAction.setEnabled(enable);
524 showTokenAgeAction.setEnabled(enable);
525+ changeNameVisibility.setEnabled(enable);
526 showAdvancedWorkspaceAction.setEnabled(enable);
527 showSimpleWorkspaceAction.setEnabled(enable);
528 saveWorkSpaceAction.setEnabled(enable);
529
530=== modified file 'src/pipe/gui/GuiFrameActions.java'
531--- src/pipe/gui/GuiFrameActions.java 2020-08-11 11:51:55 +0000
532+++ src/pipe/gui/GuiFrameActions.java 2021-08-03 08:52:27 +0000
533@@ -47,7 +47,7 @@
534 void setShowQueriesSelected(boolean b);
535 void setShowEnabledTransitionsSelected(boolean b);
536 void setShowDelayEnabledTransitionsSelected(boolean b);
537- void setShowToolTipsSelected(boolean b);
538+ void setShowToolTipsSelected(boolean b);;
539 void setShowZeroToInfinityIntervalsSelected(boolean b);
540 void setShowTokenAgeSelected(boolean b);
541
542
543=== modified file 'src/pipe/gui/GuiFrameController.java'
544--- src/pipe/gui/GuiFrameController.java 2021-04-05 10:10:17 +0000
545+++ src/pipe/gui/GuiFrameController.java 2021-08-03 08:52:27 +0000
546@@ -113,7 +113,6 @@
547 guiFrame.changeToTab(tab);
548 //XXX fixes an issue where on first open of a net the time intervals are not shown
549 tab.drawingSurface().repaintAll();
550-
551 }
552
553 //If needed, add boolean forceClose, where net is not checkedForSave and just closed
554
555=== modified file 'src/pipe/gui/canvas/DrawingSurfaceImpl.java'
556--- src/pipe/gui/canvas/DrawingSurfaceImpl.java 2020-08-11 06:00:12 +0000
557+++ src/pipe/gui/canvas/DrawingSurfaceImpl.java 2021-08-03 08:52:27 +0000
558@@ -495,9 +495,11 @@
559
560
561 public void translateSelection(ArrayList<PetriNetObject> objects, int transX, int transY) {
562- tabContent.getUndoManager().newEdit(); // new "transaction""
563- for (PetriNetObject pnobject : objects) {
564- tabContent.getUndoManager().addEdit(new TranslatePetriNetObjectEdit(pnobject, transX, transY, this));
565- }
566+ if (transX != 0 || transY != 0) {
567+ tabContent.getUndoManager().newEdit(); // new "transaction""
568+ for (PetriNetObject pnobject : objects) {
569+ tabContent.getUndoManager().addEdit(new TranslatePetriNetObjectEdit(pnobject, transX, transY, this));
570+ }
571+ }
572 }
573 }
574
575=== modified file 'src/pipe/gui/graphicElements/PlaceTransitionObject.java'
576--- src/pipe/gui/graphicElements/PlaceTransitionObject.java 2020-08-20 20:45:38 +0000
577+++ src/pipe/gui/graphicElements/PlaceTransitionObject.java 2021-08-03 08:52:27 +0000
578@@ -19,9 +19,9 @@
579 private final LinkedList<Arc> connectTo = new LinkedList<Arc>();
580 private final LinkedList<Arc> connectFrom = new LinkedList<Arc>();
581
582- protected boolean attributesVisible = false;
583+ protected boolean attributesVisible = true;
584
585- public PlaceTransitionObject(
586+ public PlaceTransitionObject(
587 double componentWidth,
588 double componentHeight,
589 int positionXInput,
590
591=== modified file 'src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java'
592--- src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2021-04-04 09:31:12 +0000
593+++ src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2021-08-03 08:52:27 +0000
594@@ -55,7 +55,6 @@
595 this.place = place;
596 this.place.addTimedPlaceListener(listener);
597 this.lens = lens;
598- attributesVisible = true;
599
600 }
601
602
603=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java'
604--- src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java 2020-08-19 11:36:09 +0000
605+++ src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java 2021-08-03 08:52:27 +0000
606@@ -42,7 +42,6 @@
607 this.transition = transition;
608 listener = timedTransitionListener();
609 transition.addTimedTransitionListener(listener);
610- attributesVisible = true;
611 this.lens = lens;
612
613 }
614
615=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
616--- src/pipe/gui/widgets/PlaceEditorPanel.java 2021-04-08 08:30:29 +0000
617+++ src/pipe/gui/widgets/PlaceEditorPanel.java 2021-08-03 08:52:27 +0000
618@@ -6,10 +6,7 @@
619 import java.awt.GridBagLayout;
620 import java.awt.Insets;
621 import java.awt.event.ItemEvent;
622-import java.util.Arrays;
623-import java.util.Collection;
624-import java.util.Set;
625-import java.util.Vector;
626+import java.util.*;
627
628 import javax.swing.ButtonGroup;
629 import javax.swing.DefaultComboBoxModel;
630@@ -23,6 +20,7 @@
631 import javax.swing.event.ChangeListener;
632
633 import dk.aau.cs.gui.TabContent;
634+import dk.aau.cs.gui.undo.*;
635 import net.tapaal.swinghelpers.CustomJSpinner;
636 import net.tapaal.swinghelpers.GridBagHelper;
637 import net.tapaal.swinghelpers.SwingHelper;
638@@ -30,16 +28,9 @@
639 import pipe.dataLayer.Template;
640 import pipe.gui.CreateGui;
641 import pipe.gui.Pipe;
642+import pipe.gui.graphicElements.PetriNetObject;
643 import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
644 import dk.aau.cs.gui.Context;
645-import dk.aau.cs.gui.undo.ChangedInvariantCommand;
646-import dk.aau.cs.gui.undo.Command;
647-import dk.aau.cs.gui.undo.MakePlaceSharedCommand;
648-import dk.aau.cs.gui.undo.MakePlaceNewSharedCommand;
649-import dk.aau.cs.gui.undo.MakePlaceNewSharedMultiCommand;
650-import dk.aau.cs.gui.undo.RenameTimedPlaceCommand;
651-import dk.aau.cs.gui.undo.TimedPlaceMarkingEdit;
652-import dk.aau.cs.gui.undo.UnsharePlaceCommand;
653 import dk.aau.cs.model.tapn.Bound.InfBound;
654 import dk.aau.cs.model.tapn.Constant;
655 import dk.aau.cs.model.tapn.ConstantBound;
656@@ -585,17 +576,19 @@
657 JOptionPane.showMessageDialog(this, "The specified name is already used by another place or transition.", "Error", JOptionPane.ERROR_MESSAGE);
658 return false;
659 }
660-
661- Command renameCommand = new RenameTimedPlaceCommand(context.tabContent(), (LocalTimedPlace)place.underlyingPlace(), oldName, newName);
662- context.undoManager().addEdit(renameCommand);
663- try{ // set name
664- renameCommand.redo();
665- }catch(RequireException e){
666- context.undoManager().undo();
667- JOptionPane.showMessageDialog(this, "Acceptable names for transitions are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*\n\nNote that \"true\" and \"false\" are reserved keywords.", "Error", JOptionPane.ERROR_MESSAGE);
668- return false;
669- }
670- context.nameGenerator().updateIndices(context.activeModel(), newName);
671+
672+ if (!oldName.equals(newName)) {
673+ Command renameCommand = new RenameTimedPlaceCommand(context.tabContent(), (LocalTimedPlace) place.underlyingPlace(), oldName, newName);
674+ context.undoManager().addEdit(renameCommand);
675+ try { // set name
676+ renameCommand.redo();
677+ } catch (RequireException e) {
678+ context.undoManager().undo();
679+ JOptionPane.showMessageDialog(this, "Acceptable names for transitions are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*\n\nNote that \"true\" and \"false\" are reserved keywords.", "Error", JOptionPane.ERROR_MESSAGE);
680+ return false;
681+ }
682+ context.nameGenerator().updateIndices(context.activeModel(), newName);
683+ }
684
685 if(makeNewShared){
686 Command command = new MakePlaceNewSharedCommand(context.activeModel(), newName, place.underlyingPlace(), place, context.tabContent(), false);
687@@ -637,6 +630,12 @@
688
689 if ((place.getAttributesVisible() && !attributesCheckBox.isSelected()) || (!place.getAttributesVisible() && attributesCheckBox.isSelected())) {
690 place.toggleAttributesVisible();
691+
692+ Map<PetriNetObject, Boolean> map = new HashMap<>();
693+ map.put(place, !place.getAttributesVisible());
694+
695+ Command changeVisibility = new ChangeAllNamesVisibilityCommand(currentTab, map, null, place.getAttributesVisible());
696+ context.undoManager().addEdit(changeVisibility);
697 }
698 place.update(true);
699 place.repaint();
700
701=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
702--- src/pipe/gui/widgets/TAPNTransitionEditor.java 2021-04-08 08:30:29 +0000
703+++ src/pipe/gui/widgets/TAPNTransitionEditor.java 2021-08-03 08:52:27 +0000
704@@ -4,6 +4,8 @@
705 import java.awt.event.ActionEvent;
706 import java.awt.event.ActionListener;
707 import java.util.ArrayList;
708+import java.util.HashMap;
709+import java.util.Map;
710 import java.util.Vector;
711
712 import javax.swing.DefaultComboBoxModel;
713@@ -21,6 +23,7 @@
714 import net.tapaal.swinghelpers.SwingHelper;
715 import net.tapaal.swinghelpers.WidthAdjustingComboBox;
716 import pipe.gui.CreateGui;
717+import pipe.gui.graphicElements.PetriNetObject;
718 import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
719 import dk.aau.cs.gui.Context;
720 import dk.aau.cs.model.tapn.Bound;
721@@ -383,11 +386,13 @@
722 }
723 try{
724 String oldName = transition.underlyingTransition().name();
725+ if (!oldName.equals(newName)) {
726 transition.underlyingTransition().setName(newName);
727 Command renameCommand = new RenameTimedTransitionCommand(context.tabContent(), transition.underlyingTransition(), oldName, newName);
728 context.undoManager().addEdit(renameCommand);
729 // set name
730 renameCommand.redo();
731+ }
732 }catch(RequireException e){
733 context.undoManager().undo();
734 JOptionPane.showMessageDialog(this,
735@@ -457,6 +462,12 @@
736
737 if(transition.getAttributesVisible() && !attributesCheckBox.isSelected() || (!transition.getAttributesVisible() && attributesCheckBox.isSelected())) {
738 transition.toggleAttributesVisible();
739+
740+ Map<PetriNetObject, Boolean> map = new HashMap<>();
741+ map.put(transition, !transition.getAttributesVisible());
742+
743+ Command changeVisibility = new ChangeAllNamesVisibilityCommand(context.tabContent(), null, map, transition.getAttributesVisible());
744+ context.undoManager().addEdit(changeVisibility);
745 }
746
747 transition.update(true);

Subscribers

People subscribed via source and target branches