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

Proposed by Lena Ernstsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1146
Merged at revision: 1130
Proposed branch: lp:~tapaal-contributor/tapaal/hide-show-names-1921393
Merge into: lp:tapaal
Diff against target: 769 lines (+439/-43)
15 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 (+11/-5)
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/QueryDialog.java (+1/-1)
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 Approve
Review via email: mp+406578@code.launchpad.net

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

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 : Posted in a previous version of this proposal

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
1145. By Lena Ernstsen

Changed tooltip for 'Merge Composed Net'

1146. By Lena Ernstsen

Changed tooltip for 'Merge Composed Net'

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/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 09:29:22 +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 09:29:22 +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 09:29:22 +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 09:29:22 +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 09:29:22 +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 09:29:22 +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@@ -241,7 +237,7 @@
499 SmartDrawDialog.showSmartDrawDialog();
500 }
501 };
502- private final GuiAction mergeComponentsDialogAction = new GuiAction("Merge net components", "Export an xml file of composed net and approximated net if enabled", KeyStroke.getKeyStroke(KeyEvent.VK_C, (shortcutkey + InputEvent.SHIFT_MASK))) {
503+ private final GuiAction mergeComponentsDialogAction = new GuiAction("Merge net components", "Open a composed net in a new tab and use approximated net if enabled", KeyStroke.getKeyStroke(KeyEvent.VK_C, (shortcutkey + InputEvent.SHIFT_MASK))) {
504 public void actionPerformed(ActionEvent e) {
505 currentTab.ifPresent(TabContentActions::mergeNetComponents);
506 }
507@@ -334,6 +330,11 @@
508 guiFrameController.ifPresent(GuiFrameControllerActions::toggleDisplayToolTips);
509 }
510 };
511+ 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) {
512+ public void actionPerformed(ActionEvent e) {
513+ currentTab.ifPresent(TabContentActions::showChangeNameVisibility);
514+ }
515+ };
516 private final GuiAction showAdvancedWorkspaceAction = new GuiAction("Show advanced workspace", "Show all panels", false) {
517 public void actionPerformed(ActionEvent e) {
518 guiFrameController.ifPresent(GuiFrameControllerActions::showAdvancedWorkspace);
519@@ -677,6 +678,10 @@
520
521 viewMenu.addSeparator();
522
523+ viewMenu.add(changeNameVisibility);
524+
525+ viewMenu.addSeparator();
526+
527 viewMenu.add(showSimpleWorkspaceAction);
528 viewMenu.add(showAdvancedWorkspaceAction);
529 viewMenu.add(saveWorkSpaceAction);
530@@ -1066,6 +1071,7 @@
531 showDelayEnabledTransitionsAction.setEnabled(enable);
532 showToolTipsAction.setEnabled(enable);
533 showTokenAgeAction.setEnabled(enable);
534+ changeNameVisibility.setEnabled(enable);
535 showAdvancedWorkspaceAction.setEnabled(enable);
536 showSimpleWorkspaceAction.setEnabled(enable);
537 saveWorkSpaceAction.setEnabled(enable);
538
539=== modified file 'src/pipe/gui/GuiFrameActions.java'
540--- src/pipe/gui/GuiFrameActions.java 2020-08-11 11:51:55 +0000
541+++ src/pipe/gui/GuiFrameActions.java 2021-08-03 09:29:22 +0000
542@@ -47,7 +47,7 @@
543 void setShowQueriesSelected(boolean b);
544 void setShowEnabledTransitionsSelected(boolean b);
545 void setShowDelayEnabledTransitionsSelected(boolean b);
546- void setShowToolTipsSelected(boolean b);
547+ void setShowToolTipsSelected(boolean b);;
548 void setShowZeroToInfinityIntervalsSelected(boolean b);
549 void setShowTokenAgeSelected(boolean b);
550
551
552=== modified file 'src/pipe/gui/GuiFrameController.java'
553--- src/pipe/gui/GuiFrameController.java 2021-04-05 10:10:17 +0000
554+++ src/pipe/gui/GuiFrameController.java 2021-08-03 09:29:22 +0000
555@@ -113,7 +113,6 @@
556 guiFrame.changeToTab(tab);
557 //XXX fixes an issue where on first open of a net the time intervals are not shown
558 tab.drawingSurface().repaintAll();
559-
560 }
561
562 //If needed, add boolean forceClose, where net is not checkedForSave and just closed
563
564=== modified file 'src/pipe/gui/canvas/DrawingSurfaceImpl.java'
565--- src/pipe/gui/canvas/DrawingSurfaceImpl.java 2020-08-11 06:00:12 +0000
566+++ src/pipe/gui/canvas/DrawingSurfaceImpl.java 2021-08-03 09:29:22 +0000
567@@ -495,9 +495,11 @@
568
569
570 public void translateSelection(ArrayList<PetriNetObject> objects, int transX, int transY) {
571- tabContent.getUndoManager().newEdit(); // new "transaction""
572- for (PetriNetObject pnobject : objects) {
573- tabContent.getUndoManager().addEdit(new TranslatePetriNetObjectEdit(pnobject, transX, transY, this));
574- }
575+ if (transX != 0 || transY != 0) {
576+ tabContent.getUndoManager().newEdit(); // new "transaction""
577+ for (PetriNetObject pnobject : objects) {
578+ tabContent.getUndoManager().addEdit(new TranslatePetriNetObjectEdit(pnobject, transX, transY, this));
579+ }
580+ }
581 }
582 }
583
584=== modified file 'src/pipe/gui/graphicElements/PlaceTransitionObject.java'
585--- src/pipe/gui/graphicElements/PlaceTransitionObject.java 2020-08-20 20:45:38 +0000
586+++ src/pipe/gui/graphicElements/PlaceTransitionObject.java 2021-08-03 09:29:22 +0000
587@@ -19,9 +19,9 @@
588 private final LinkedList<Arc> connectTo = new LinkedList<Arc>();
589 private final LinkedList<Arc> connectFrom = new LinkedList<Arc>();
590
591- protected boolean attributesVisible = false;
592+ protected boolean attributesVisible = true;
593
594- public PlaceTransitionObject(
595+ public PlaceTransitionObject(
596 double componentWidth,
597 double componentHeight,
598 int positionXInput,
599
600=== modified file 'src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java'
601--- src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2021-04-04 09:31:12 +0000
602+++ src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2021-08-03 09:29:22 +0000
603@@ -55,7 +55,6 @@
604 this.place = place;
605 this.place.addTimedPlaceListener(listener);
606 this.lens = lens;
607- attributesVisible = true;
608
609 }
610
611
612=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java'
613--- src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java 2020-08-19 11:36:09 +0000
614+++ src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java 2021-08-03 09:29:22 +0000
615@@ -42,7 +42,6 @@
616 this.transition = transition;
617 listener = timedTransitionListener();
618 transition.addTimedTransitionListener(listener);
619- attributesVisible = true;
620 this.lens = lens;
621
622 }
623
624=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
625--- src/pipe/gui/widgets/PlaceEditorPanel.java 2021-04-08 08:30:29 +0000
626+++ src/pipe/gui/widgets/PlaceEditorPanel.java 2021-08-03 09:29:22 +0000
627@@ -6,10 +6,7 @@
628 import java.awt.GridBagLayout;
629 import java.awt.Insets;
630 import java.awt.event.ItemEvent;
631-import java.util.Arrays;
632-import java.util.Collection;
633-import java.util.Set;
634-import java.util.Vector;
635+import java.util.*;
636
637 import javax.swing.ButtonGroup;
638 import javax.swing.DefaultComboBoxModel;
639@@ -23,6 +20,7 @@
640 import javax.swing.event.ChangeListener;
641
642 import dk.aau.cs.gui.TabContent;
643+import dk.aau.cs.gui.undo.*;
644 import net.tapaal.swinghelpers.CustomJSpinner;
645 import net.tapaal.swinghelpers.GridBagHelper;
646 import net.tapaal.swinghelpers.SwingHelper;
647@@ -30,16 +28,9 @@
648 import pipe.dataLayer.Template;
649 import pipe.gui.CreateGui;
650 import pipe.gui.Pipe;
651+import pipe.gui.graphicElements.PetriNetObject;
652 import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
653 import dk.aau.cs.gui.Context;
654-import dk.aau.cs.gui.undo.ChangedInvariantCommand;
655-import dk.aau.cs.gui.undo.Command;
656-import dk.aau.cs.gui.undo.MakePlaceSharedCommand;
657-import dk.aau.cs.gui.undo.MakePlaceNewSharedCommand;
658-import dk.aau.cs.gui.undo.MakePlaceNewSharedMultiCommand;
659-import dk.aau.cs.gui.undo.RenameTimedPlaceCommand;
660-import dk.aau.cs.gui.undo.TimedPlaceMarkingEdit;
661-import dk.aau.cs.gui.undo.UnsharePlaceCommand;
662 import dk.aau.cs.model.tapn.Bound.InfBound;
663 import dk.aau.cs.model.tapn.Constant;
664 import dk.aau.cs.model.tapn.ConstantBound;
665@@ -585,17 +576,19 @@
666 JOptionPane.showMessageDialog(this, "The specified name is already used by another place or transition.", "Error", JOptionPane.ERROR_MESSAGE);
667 return false;
668 }
669-
670- Command renameCommand = new RenameTimedPlaceCommand(context.tabContent(), (LocalTimedPlace)place.underlyingPlace(), oldName, newName);
671- context.undoManager().addEdit(renameCommand);
672- try{ // set name
673- renameCommand.redo();
674- }catch(RequireException e){
675- context.undoManager().undo();
676- 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);
677- return false;
678- }
679- context.nameGenerator().updateIndices(context.activeModel(), newName);
680+
681+ if (!oldName.equals(newName)) {
682+ Command renameCommand = new RenameTimedPlaceCommand(context.tabContent(), (LocalTimedPlace) place.underlyingPlace(), oldName, newName);
683+ context.undoManager().addEdit(renameCommand);
684+ try { // set name
685+ renameCommand.redo();
686+ } catch (RequireException e) {
687+ context.undoManager().undo();
688+ 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);
689+ return false;
690+ }
691+ context.nameGenerator().updateIndices(context.activeModel(), newName);
692+ }
693
694 if(makeNewShared){
695 Command command = new MakePlaceNewSharedCommand(context.activeModel(), newName, place.underlyingPlace(), place, context.tabContent(), false);
696@@ -637,6 +630,12 @@
697
698 if ((place.getAttributesVisible() && !attributesCheckBox.isSelected()) || (!place.getAttributesVisible() && attributesCheckBox.isSelected())) {
699 place.toggleAttributesVisible();
700+
701+ Map<PetriNetObject, Boolean> map = new HashMap<>();
702+ map.put(place, !place.getAttributesVisible());
703+
704+ Command changeVisibility = new ChangeAllNamesVisibilityCommand(currentTab, map, null, place.getAttributesVisible());
705+ context.undoManager().addEdit(changeVisibility);
706 }
707 place.update(true);
708 place.repaint();
709
710=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
711--- src/pipe/gui/widgets/QueryDialog.java 2021-03-29 10:08:13 +0000
712+++ src/pipe/gui/widgets/QueryDialog.java 2021-08-03 09:29:22 +0000
713@@ -314,7 +314,7 @@
714 private final static String TOOL_TIP_SAVE_AND_VERIFY_BUTTON = "Save and verify the query.";
715 private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";
716 private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";
717- private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
718+ private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Open a composed net in a new tab and use approximated net if enabled";
719 private final static String TOOL_TIP_OPEN_REDUCED_BUTTON = "Open the net produced after applying structural reduction rules";
720 private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
721 private final static String TOOL_TIP_SAVE_PN_BUTTON = "Export an xml file that can be used as input for the untimed Petri net engine.";
722
723=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
724--- src/pipe/gui/widgets/TAPNTransitionEditor.java 2021-04-08 08:30:29 +0000
725+++ src/pipe/gui/widgets/TAPNTransitionEditor.java 2021-08-03 09:29:22 +0000
726@@ -4,6 +4,8 @@
727 import java.awt.event.ActionEvent;
728 import java.awt.event.ActionListener;
729 import java.util.ArrayList;
730+import java.util.HashMap;
731+import java.util.Map;
732 import java.util.Vector;
733
734 import javax.swing.DefaultComboBoxModel;
735@@ -21,6 +23,7 @@
736 import net.tapaal.swinghelpers.SwingHelper;
737 import net.tapaal.swinghelpers.WidthAdjustingComboBox;
738 import pipe.gui.CreateGui;
739+import pipe.gui.graphicElements.PetriNetObject;
740 import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
741 import dk.aau.cs.gui.Context;
742 import dk.aau.cs.model.tapn.Bound;
743@@ -383,11 +386,13 @@
744 }
745 try{
746 String oldName = transition.underlyingTransition().name();
747+ if (!oldName.equals(newName)) {
748 transition.underlyingTransition().setName(newName);
749 Command renameCommand = new RenameTimedTransitionCommand(context.tabContent(), transition.underlyingTransition(), oldName, newName);
750 context.undoManager().addEdit(renameCommand);
751 // set name
752 renameCommand.redo();
753+ }
754 }catch(RequireException e){
755 context.undoManager().undo();
756 JOptionPane.showMessageDialog(this,
757@@ -457,6 +462,12 @@
758
759 if(transition.getAttributesVisible() && !attributesCheckBox.isSelected() || (!transition.getAttributesVisible() && attributesCheckBox.isSelected())) {
760 transition.toggleAttributesVisible();
761+
762+ Map<PetriNetObject, Boolean> map = new HashMap<>();
763+ map.put(transition, !transition.getAttributesVisible());
764+
765+ Command changeVisibility = new ChangeAllNamesVisibilityCommand(context.tabContent(), null, map, transition.getAttributesVisible());
766+ context.undoManager().addEdit(changeVisibility);
767 }
768
769 transition.update(true);

Subscribers

People subscribed via source and target branches