Merge lp:~tapaal-contributor/tapaal/hide-show-names-1921393 into lp:tapaal
- hide-show-names-1921393
- Merge into trunk
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 | ||||
Related bugs: |
|
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.
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
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).
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).
- 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
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); |
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).