Merge lp:~yrke/tapaal/guirefactor into lp:tapaal

Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1139
Merged at revision: 965
Proposed branch: lp:~yrke/tapaal/guirefactor
Merge into: lp:tapaal
Diff against target: 8661 lines (+2256/-3444)
88 files modified
src/dk/aau/cs/gui/BatchProcessingDialog.java (+4/-11)
src/dk/aau/cs/gui/DrawingSurface.java (+0/-11)
src/dk/aau/cs/gui/TabComponent.java (+2/-13)
src/dk/aau/cs/gui/TabContent.java (+43/-43)
src/dk/aau/cs/gui/TemplateExplorer.java (+10/-10)
src/dk/aau/cs/gui/components/PetriNetElementControl.java (+0/-105)
src/dk/aau/cs/gui/components/TextLabel.java (+0/-90)
src/dk/aau/cs/gui/components/TimedPlaceControl.java (+0/-200)
src/dk/aau/cs/gui/components/handlers/ClickHandler.java (+0/-34)
src/dk/aau/cs/gui/components/handlers/DragHandler.java (+0/-50)
src/dk/aau/cs/gui/undo/AddPetriNetControlCommand.java (+0/-29)
src/dk/aau/cs/io/TraceImportExport.java (+5/-5)
src/dk/aau/cs/util/JavaUtil.java (+23/-0)
src/dk/aau/cs/util/Require.java (+5/-0)
src/dk/aau/cs/verification/UPPAAL/Verifyta.java (+2/-6)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+2/-6)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+2/-4)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java (+2/-3)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+6/-6)
src/net/tapaal/TAPAAL.java (+7/-2)
src/pipe/dataLayer/DataLayer.java (+1/-8)
src/pipe/dataLayer/Template.java (+1/-1)
src/pipe/gui/AnimationController.java (+178/-244)
src/pipe/gui/AnimationHistoryComponent.java (+5/-5)
src/pipe/gui/AnimationSettings.java (+1/-1)
src/pipe/gui/Animator.java (+24/-24)
src/pipe/gui/CreateGui.java (+42/-299)
src/pipe/gui/DelayEnabledTransitionControl.java (+10/-10)
src/pipe/gui/DrawingSurfaceImpl.java (+25/-32)
src/pipe/gui/Export.java (+8/-9)
src/pipe/gui/ExportBatchDialog.java (+3/-6)
src/pipe/gui/ExtensionFilter.java (+0/-32)
src/pipe/gui/FileFinder.java (+11/-2)
src/pipe/gui/FileFinderImpl.java (+0/-15)
src/pipe/gui/GuiFrame.java (+1383/-1429)
src/pipe/gui/Pipe.java (+4/-22)
src/pipe/gui/RunVerificationBase.java (+1/-12)
src/pipe/gui/SimulationControl.java (+3/-3)
src/pipe/gui/SimulatorFocusTraversalPolicy.java (+3/-3)
src/pipe/gui/StatusBar.java (+23/-26)
src/pipe/gui/Verifier.java (+4/-4)
src/pipe/gui/action/DeletePetriNetObjectAction.java (+0/-98)
src/pipe/gui/action/EditAnnotationBorderAction.java (+1/-1)
src/pipe/gui/action/GuiAction.java (+33/-13)
src/pipe/gui/action/InsertPointAction.java (+0/-41)
src/pipe/gui/action/SplitArcAction.java (+1/-1)
src/pipe/gui/action/SplitArcPointAction.java (+1/-1)
src/pipe/gui/action/ToggleArcPointAction.java (+1/-1)
src/pipe/gui/graphicElements/AnnotationNote.java (+2/-2)
src/pipe/gui/graphicElements/Arc.java (+2/-2)
src/pipe/gui/graphicElements/Note.java (+2/-2)
src/pipe/gui/graphicElements/PetriNetObject.java (+1/-7)
src/pipe/gui/graphicElements/Place.java (+1/-1)
src/pipe/gui/graphicElements/Transition.java (+1/-1)
src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java (+2/-2)
src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+1/-1)
src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java (+2/-2)
src/pipe/gui/handler/ArcHandler.java (+1/-1)
src/pipe/gui/handler/ArcPathPointHandler.java (+1/-1)
src/pipe/gui/handler/LabelHandler.java (+1/-1)
src/pipe/gui/handler/PetriNetObjectHandler.java (+2/-4)
src/pipe/gui/handler/PlaceHandler.java (+3/-5)
src/pipe/gui/handler/PlaceTransitionObjectHandler.java (+5/-5)
src/pipe/gui/handler/SpecialMacHandler.java (+3/-3)
src/pipe/gui/handler/TAPNTransitionHandler.java (+1/-1)
src/pipe/gui/handler/TransitionHandler.java (+4/-5)
src/pipe/gui/undo/AddConstantEdit.java (+2/-2)
src/pipe/gui/undo/DeleteTimedPlaceCommand.java (+1/-1)
src/pipe/gui/undo/RemoveConstantEdit.java (+2/-2)
src/pipe/gui/undo/UpdateConstantEdit.java (+2/-2)
src/pipe/gui/widgets/CTLQueryDialog.java (+4/-4)
src/pipe/gui/widgets/ConstantsDialogPanel.java (+1/-1)
src/pipe/gui/widgets/ConstantsPane.java (+2/-21)
src/pipe/gui/widgets/EngineDialogPanel.java (+10/-14)
src/pipe/gui/widgets/FileBrowser.java (+0/-49)
src/pipe/gui/widgets/FileBrowserImplementation.java (+0/-16)
src/pipe/gui/widgets/GuardDialogue.java (+1/-3)
src/pipe/gui/widgets/NativeFileBrowser.java (+0/-130)
src/pipe/gui/widgets/NativeFileBrowserFallback.java (+0/-132)
src/pipe/gui/widgets/NewTAPNPanel.java (+1/-1)
src/pipe/gui/widgets/PlaceEditorPanel.java (+3/-12)
src/pipe/gui/widgets/QueryDialog.java (+4/-11)
src/pipe/gui/widgets/QueryPane.java (+2/-14)
src/pipe/gui/widgets/TAPNTransitionEditor.java (+0/-1)
src/pipe/gui/widgets/WorkflowDialog.java (+2/-11)
src/pipe/gui/widgets/filebrowser/FileBrowser.java (+50/-0)
src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java (+122/-0)
src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java (+132/-0)
To merge this branch: bzr merge lp:~yrke/tapaal/guirefactor
Reviewer Review Type Date Requested Status
Jiri Srba Approve
TAPAAL Reviewers Pending
Review via email: mp+348880@code.launchpad.net

Commit message

General GUI refactoring and improvements.

To post a comment you must log in.
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

Please test loading of PNML files

lp:~yrke/tapaal/guirefactor updated
1137. By Kenneth Yrke Jørgensen

Merged branch, Implements zoome using scrollwheel with ctrl

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

Does not compile:

javac -source 1.6 -target 1.6 -sourcepath src -cp libs/\* -d classes/ 'src/TAPAAL.java' -encoding UTF8
warning: [options] bootstrap class path not set in conjunction with -source 1.6
src/pipe/gui/GuiFrame.java:2602: error: local variable filename is accessed from within inner class; needs to be declared final
       InputStream file = Thread.currentThread().getContextClassLoader().getResourceAsStream("resources/Example nets/" + filename);
                                                                                                                         ^
src/pipe/gui/GuiFrame.java:2603: error: local variable netname is accessed from within inner class; needs to be declared final
       createNewTabFromFile(file, netname);
                                  ^
Note: Some input files use or override a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
2 errors
1 warning
make: *** [release] Error 1

review: Needs Fixing
lp:~yrke/tapaal/guirefactor updated
1138. By Kenneth Yrke Jørgensen

fixed closure to use final variable to allow to compile to java 1.6

Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

Added fix to support java 1.6. Please test the loading of examples nets when running TAPAAL from a Jar file.

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

Closing of a tab on Mac was before possible using cmd-W but now it does not work anymore (it requires ctrl-W). The same problem is for cmd-O (open net) and cmd-N (new net) that does not work
any more and requires ctrl instead, which is not the usual way on Mac. It used to work ok before.

review: Needs Fixing
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

Hmm... shortcuts has been overwritten ala:

saveAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('S', shortcutkey));

instead of setting them in the correct way, should be a relative simple fix.

lp:~yrke/tapaal/guirefactor updated
1139. By Kenneth Yrke Jørgensen

Fixed some actions using hardcoded ctrl as shortcutkey

Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

Fixed shortcuts for select all, new net, open net, close net, and save as. Now set using the correct method instead of being overwritten.

Search for all places with hardcoded ctrl hotkey, no more found.

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

Shortcuts work as they should and loading example nets from jar file tested.

The ctrl-scrollwheel zoom works with mouse on Mac but is does not quite work
with the touchpad on macbookpro (it shrinks the net but enlarging it again just makes the net
to "jump" but after releasing the touch it gets back to its minimum size).

Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

interesting, might be related to how events are handled. Also im unsure what happens on a PC using the touchpad or similar, some machines this might be seen as a differenct kind of actions.

On macOS what are the conventions on zooming behaviour?

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

Tested on mac and all seems to work fine, so I am going to merge it to trunk.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/gui/BatchProcessingDialog.java'
2--- src/dk/aau/cs/gui/BatchProcessingDialog.java 2018-04-21 11:58:41 +0000
3+++ src/dk/aau/cs/gui/BatchProcessingDialog.java 2018-07-04 11:38:47 +0000
4@@ -31,7 +31,6 @@
5 import javax.swing.JCheckBox;
6 import javax.swing.JComboBox;
7 import javax.swing.JDialog;
8-import javax.swing.JFileChooser;
9 import javax.swing.JLabel;
10 import javax.swing.JList;
11 import javax.swing.JOptionPane;
12@@ -54,7 +53,6 @@
13 import javax.swing.event.ListSelectionListener;
14 import javax.swing.event.TableModelEvent;
15 import javax.swing.event.TableModelListener;
16-import javax.swing.filechooser.FileNameExtensionFilter;
17 import javax.swing.table.TableCellRenderer;
18 import javax.swing.table.TableModel;
19 import javax.swing.table.TableRowSorter;
20@@ -62,10 +60,9 @@
21 import pipe.dataLayer.TAPNQuery;
22 import pipe.dataLayer.TAPNQuery.SearchOption;
23 import pipe.gui.CreateGui;
24-import pipe.gui.FileFinderImpl;
25 import pipe.gui.widgets.CustomJSpinner;
26 import pipe.gui.widgets.EscapableDialog;
27-import pipe.gui.widgets.FileBrowser;
28+import pipe.gui.widgets.filebrowser.FileBrowser;
29 import pipe.gui.widgets.QueryPane;
30 import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
31 import dk.aau.cs.gui.components.BatchProcessingResultsTableModel;
32@@ -75,11 +72,7 @@
33 import dk.aau.cs.translations.ReductionOption;
34 import dk.aau.cs.util.MemoryMonitor;
35 import dk.aau.cs.util.StringComparator;
36-import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
37 import dk.aau.cs.verification.VerificationOptions;
38-import dk.aau.cs.verification.VerifyTAPN.VerifyDTAPNOptions;
39-import dk.aau.cs.verification.VerifyTAPN.VerifyPNOptions;
40-import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
41 import dk.aau.cs.verification.batchProcessing.BatchProcessingListener;
42 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions;
43 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.ApproximationMethodOption;
44@@ -512,7 +505,7 @@
45 }
46
47 private void addFiles() {
48- FileBrowser browser = new FileBrowser("Timed-Arc Petri Nets","xml", lastPath);
49+ FileBrowser browser = FileBrowser.constructor("Timed-Arc Petri Nets","xml", lastPath);
50
51 File[] filesArray = browser.openFiles();
52 if (filesArray.length>0) {
53@@ -1026,7 +1019,7 @@
54 }
55
56 private void exportResults() {
57- String filename = new FileBrowser("CSV file", "csv", lastPath)
58+ String filename = FileBrowser.constructor("CSV file", "csv", lastPath)
59 .saveFile("results");
60 if (filename != null) {
61 File exportFile = new File(filename);
62@@ -1384,7 +1377,7 @@
63
64 public void fireFileChanged(FileChangedEvent e) {
65 if(!(isQueryListEmpty())) {
66- fileStatusLabel.setText(CreateGui.appGui.getCurrentTabName());
67+ fileStatusLabel.setText(CreateGui.getAppGui().getCurrentTabName());
68 }
69 else
70 fileStatusLabel.setText(e.fileName());
71
72=== removed file 'src/dk/aau/cs/gui/DrawingSurface.java'
73--- src/dk/aau/cs/gui/DrawingSurface.java 2011-02-03 19:03:15 +0000
74+++ src/dk/aau/cs/gui/DrawingSurface.java 1970-01-01 00:00:00 +0000
75@@ -1,11 +0,0 @@
76-package dk.aau.cs.gui;
77-
78-import java.awt.Component;
79-
80-public interface DrawingSurface {
81- void updatePreferredSize();
82-
83- Component add(Component component);
84-
85- void remove(Component component);
86-}
87
88=== modified file 'src/dk/aau/cs/gui/TabComponent.java'
89--- src/dk/aau/cs/gui/TabComponent.java 2016-02-15 10:28:53 +0000
90+++ src/dk/aau/cs/gui/TabComponent.java 2018-07-04 11:38:47 +0000
91@@ -72,7 +72,7 @@
92 public TabComponent(final JTabbedPane pane) {
93 super(new FlowLayout(FlowLayout.LEFT, 0, 0));
94
95- Require.that(pane != null, "TabbedPane is null");
96+ Require.notNull(pane, "TabbedPane is null");
97
98 this.pane = pane;
99 setOpaque(false);
100@@ -116,18 +116,7 @@
101 addActionListener(new ActionListener(){
102 public void actionPerformed(ActionEvent arg0) {
103 int index = pane.indexOfTabComponent(TabComponent.this);
104- if(pane.getTabCount() > 0 && CreateGui.getApp().checkForSave(index)){
105- if(pane.getTabCount() == 1) { CreateGui.getApp().setGUIMode(GUIMode.noNet); }
106-
107- //Close the gui part first, else we get an error bug #826578
108- pane.removeTabAt(index);
109- CreateGui.removeTab(index);
110-
111- //Update DrawingSurfaceImpl manually. Bug #1543124
112- CreateGui.getApp().setObjects(pane.getSelectedIndex());
113-
114- CreateGui.getApp().activateSelectAction();
115- }
116+ CreateGui.getApp().closeTab(index);
117 }
118 });
119 }
120
121=== modified file 'src/dk/aau/cs/gui/TabContent.java'
122--- src/dk/aau/cs/gui/TabContent.java 2018-03-27 07:52:47 +0000
123+++ src/dk/aau/cs/gui/TabContent.java 2018-07-04 11:38:47 +0000
124@@ -50,25 +50,25 @@
125 public class TabContent extends JSplitPane {
126 private static final long serialVersionUID = -648006317150905097L;
127
128- protected TimedArcPetriNetNetwork tapnNetwork = new TimedArcPetriNetNetwork();
129- protected HashMap<TimedArcPetriNet, DataLayer> guiModels = new HashMap<TimedArcPetriNet, DataLayer>();
130- protected HashMap<TimedArcPetriNet, Zoomer> zoomLevels = new HashMap<TimedArcPetriNet, Zoomer>();
131- protected JScrollPane drawingSurfaceScroller;
132- protected JScrollPane editorSplitPaneScroller;
133- protected JScrollPane animatorSplitPaneScroller;
134- protected DrawingSurfaceImpl drawingSurface;
135- protected File appFile;
136+ private TimedArcPetriNetNetwork tapnNetwork = new TimedArcPetriNetNetwork();
137+ private HashMap<TimedArcPetriNet, DataLayer> guiModels = new HashMap<TimedArcPetriNet, DataLayer>();
138+ private HashMap<TimedArcPetriNet, Zoomer> zoomLevels = new HashMap<TimedArcPetriNet, Zoomer>();
139+ private JScrollPane drawingSurfaceScroller;
140+ private JScrollPane editorSplitPaneScroller;
141+ private JScrollPane animatorSplitPaneScroller;
142+ private DrawingSurfaceImpl drawingSurface;
143+ private File appFile;
144 private JPanel drawingSurfaceDummy;
145
146 // Normal mode
147- BugHandledJXMultisplitPane editorSplitPane;
148- static Split editorModelroot = null;
149- static Split simulatorModelRoot = null;
150+ private BugHandledJXMultisplitPane editorSplitPane;
151+ private static Split editorModelroot = null;
152+ private static Split simulatorModelRoot = null;
153
154- QueryPane queries;
155- ConstantsPane constantsPanel;
156- TemplateExplorer templateExplorer;
157- SharedPlacesAndTransitionsPanel sharedPTPanel;
158+ private QueryPane queries;
159+ private ConstantsPane constantsPanel;
160+ private TemplateExplorer templateExplorer;
161+ private SharedPlacesAndTransitionsPanel sharedPTPanel;
162
163 private static final String constantsName = "constants";
164 private static final String queriesName = "queries";
165@@ -76,28 +76,25 @@
166 private static final String sharedPTName = "sharedPT";
167
168 // / Animation
169- protected AnimationHistoryComponent animBox;
170- protected AnimationController animControlerBox;
171- protected JScrollPane animationHistoryScrollPane;
172- protected JScrollPane animationControllerScrollPane;
173- protected AnimationHistoryComponent abstractAnimationPane = null;
174- protected JPanel animationControlsPanel;
175- protected TransitionFireingComponent transitionFireing;
176+ private AnimationHistoryComponent animBox;
177+ private AnimationController animControlerBox;
178+ private JScrollPane animationHistoryScrollPane;
179+ private JScrollPane animationControllerScrollPane;
180+ private AnimationHistoryComponent abstractAnimationPane = null;
181+ private JPanel animationControlsPanel;
182+ private TransitionFireingComponent transitionFireing;
183
184 private static final String transitionFireingName = "enabledTransitions";
185 private static final String animControlName = "animControl";
186
187- protected JSplitPane animationHistorySplitter;
188+ private JSplitPane animationHistorySplitter;
189
190- protected BugHandledJXMultisplitPane animatorSplitPane;
191+ private BugHandledJXMultisplitPane animatorSplitPane;
192
193 private Integer selectedTemplate = 0;
194 private Boolean selectedTemplateWasActive = false;
195
196 private WorkflowDialog workflowDialog = null;
197-
198- //Some nets are so big we can't draw them
199- private boolean showDrawingSurface;
200
201 public TabContent(NetType netType) {
202 for (TimedArcPetriNet net : tapnNetwork.allTemplates()) {
203@@ -139,7 +136,6 @@
204 this.setOneTouchExpandable(true);
205 this.setBorder(null); // avoid multiple borders
206 this.setDividerSize(8);
207-
208 }
209
210 public SharedPlacesAndTransitionsPanel getSharedPlacesAndTransitionsPanel(){
211@@ -298,14 +294,14 @@
212 for (int i = 0; i < Math.abs(steps); i++) {
213 animBox.stepBackwards();
214 anim.stepBack();
215- CreateGui.getAnimationController()
216+ CreateGui.getCurrentTab().getAnimationController()
217 .setAnimationButtonsEnabled();
218 }
219 } else {
220 for (int i = 0; i < Math.abs(steps); i++) {
221 animBox.stepForward();
222 anim.stepForward();
223- CreateGui.getAnimationController()
224+ CreateGui.getCurrentTab().getAnimationController()
225 .setAnimationButtonsEnabled();
226 }
227 }
228@@ -325,8 +321,6 @@
229 //Add 10 pixel to the minimumsize of the scrollpane
230 animationHistoryScrollPane.setMinimumSize(new Dimension(animationHistoryScrollPane.getMinimumSize().width, animationHistoryScrollPane.getMinimumSize().height + 20));
231 }
232-
233- private final static String delayEnabledTransitionControlName = "delayEnabledTransitionControl";
234
235 private void createAnimatorSplitPane(NetType netType) {
236 if (animBox == null)
237@@ -399,8 +393,7 @@
238 animatorSplitPane.add(templateExplorer, templateExplorerName);
239
240 // Inserts dummy to avoid nullpointerexceptions from the displaynode
241- // method
242- // A component can only be on one splitpane at the time
243+ // method. A component can only be on one splitpane at the time
244 dummy = new JButton("EditorDummy");
245 dummy.setMinimumSize(templateExplorer.getMinimumSize());
246 dummy.setPreferredSize(templateExplorer.getPreferredSize());
247@@ -410,7 +403,6 @@
248 showEnabledTransitionsList(showEnabledTransitions);
249
250 this.setLeftComponent(animatorSplitPaneScroller);
251- animatorSplitPaneScroller.setPreferredSize(editorSplitPaneScroller.getSize());
252
253 }
254
255@@ -427,8 +419,7 @@
256 if (animatorSplitPane != null) {
257
258 // Inserts dummy to avoid nullpointerexceptions from the displaynode
259- // method
260- // A component can only be on one splitpane at the time
261+ // method. A component can only be on one splitpane at the time
262 dummy = new JButton("AnimatorDummy");
263 dummy.setMinimumSize(templateExplorer.getMinimumSize());
264 dummy.setPreferredSize(templateExplorer.getPreferredSize());
265@@ -437,7 +428,6 @@
266
267 templateExplorer.switchToEditorMode();
268 this.setLeftComponent(editorSplitPaneScroller);
269- editorSplitPaneScroller.setPreferredSize(animatorSplitPaneScroller.getSize());
270 drawingSurface.repaintAll();
271 }
272
273@@ -494,7 +484,6 @@
274 gbc.weighty = 1.0;
275 animationControlsPanel.add(animationHistoryScrollPane, gbc);
276 animatorSplitPane.validate();
277-
278 }
279
280 private void createAnimationController(NetType netType) {
281@@ -554,11 +543,24 @@
282 return count;
283 }
284
285- public void addTemplate(Template template) {
286+ /*
287+ XXX: 2018-05-07 kyrke, added a version of addTemplate that does not call templatExplorer.updatTemplateList
288+ used in createNewTab (as updateTamplateList expects the current tab to be selected)
289+ this needs to be refactored asap. but the is the only way I could get it to work for now.
290+ The code is very unclean on what is a template, TimeArcPetriNetNetwork, seems to mix concerns about
291+ gui/controller/model. Further refactoring is needed to clean up this mess.
292+ */
293+ public void addTemplate(Template template, boolean updateTemplateExplorer) {
294 tapnNetwork.add(template.model());
295 guiModels.put(template.model(), template.guiModel());
296 zoomLevels.put(template.model(), template.zoomer());
297- templateExplorer.updateTemplateList();
298+ if (updateTemplateExplorer) {
299+ templateExplorer.updateTemplateList();
300+ }
301+ }
302+
303+ public void addTemplate(Template template) {
304+ addTemplate(template, true);
305 }
306
307 public void addGuiModel(TimedArcPetriNet net, DataLayer guiModel) {
308@@ -599,7 +601,6 @@
309
310 public void setConstants(Iterable<Constant> constants) {
311 tapnNetwork.setConstants(constants);
312- // constantsPanel.showConstants();
313 }
314
315 public void setupNameGeneratorsFromTemplates(Iterable<Template> templates) {
316@@ -703,7 +704,6 @@
317 templateExplorer.selectFirst();
318 queries.selectFirst();
319 constantsPanel.selectFirst();
320-
321 }
322
323 public boolean isQueryPossible() {
324
325=== modified file 'src/dk/aau/cs/gui/TemplateExplorer.java'
326--- src/dk/aau/cs/gui/TemplateExplorer.java 2017-03-12 00:33:00 +0000
327+++ src/dk/aau/cs/gui/TemplateExplorer.java 2018-07-04 11:38:47 +0000
328@@ -126,7 +126,7 @@
329 }
330
331 public Integer indexOfSelectedTemplate() {
332- return new Integer(templateList.getSelectedIndex());
333+ return templateList.getSelectedIndex();
334 }
335
336 public void restoreSelectedTemplate(Integer value) {
337@@ -476,14 +476,14 @@
338 }
339
340 private EscapableDialog dialog;
341- JPanel container;
342- JTextField nameTextField;
343- Dimension size;
344- JLabel nameLabel;
345- JPanel buttonContainer;
346- JButton okButton;
347- JButton cancelButton;
348- JPanel nameContainer;
349+ private JPanel container;
350+ private JTextField nameTextField;
351+ private Dimension size;
352+ private JLabel nameLabel;
353+ private JPanel buttonContainer;
354+ private JButton okButton;
355+ private JButton cancelButton;
356+ private JPanel nameContainer;
357
358 private void onOKRenameTemplate() {
359 Template template = selectedModel();
360@@ -928,7 +928,7 @@
361 JOptionPane.showMessageDialog(parent, "At least one component must be active.", "Cannot Deactive All Components", JOptionPane.INFORMATION_MESSAGE);
362 } else {
363 //The change was ok, record it to undo/redo history
364- undoManager.addNewEdit(new ToggleTemplateActivationCommand(parent.templateExplorer, item, newValue));
365+ undoManager.addNewEdit(new ToggleTemplateActivationCommand(parent.getTemplateExplorer(), item, newValue));
366 }
367
368
369
370=== removed file 'src/dk/aau/cs/gui/components/PetriNetElementControl.java'
371--- src/dk/aau/cs/gui/components/PetriNetElementControl.java 2011-06-28 16:30:37 +0000
372+++ src/dk/aau/cs/gui/components/PetriNetElementControl.java 1970-01-01 00:00:00 +0000
373@@ -1,105 +0,0 @@
374-package dk.aau.cs.gui.components;
375-
376-import java.awt.Graphics;
377-import java.awt.Point;
378-
379-import javax.swing.JComponent;
380-import javax.swing.JPopupMenu;
381-
382-import pipe.gui.Pipe;
383-import dk.aau.cs.gui.DrawingSurface;
384-
385-public abstract class PetriNetElementControl extends JComponent {
386- private static final long serialVersionUID = -3429746860537818157L;
387-
388- private Point originalLocation;
389- private final DrawingSurface parent;
390-
391- private boolean selected = false;
392-
393- public PetriNetElementControl(DrawingSurface parent, Point originalLocation) {
394- this.parent = parent;
395- this.originalLocation = originalLocation;
396- }
397-
398- public boolean isSelected() {
399- return selected;
400- }
401-
402- protected DrawingSurface parent() {
403- return parent;
404- }
405-
406- public void select() {
407- if (!selected) {
408- selected = true;
409- selectChildren();
410- repaint();
411- }
412- }
413-
414- public void deselect() {
415- if (selected) {
416- selected = false;
417- deselectChildren();
418- repaint();
419- }
420- }
421-
422- public void zoom(int percentage) {
423- double scaleFactor = percentage / 100.0;
424-
425- double positionX = originalLocation.x * scaleFactor;
426- double positionY = originalLocation.y * scaleFactor;
427- double width = Pipe.PLACE_TRANSITION_HEIGHT * scaleFactor;
428- double height = Pipe.PLACE_TRANSITION_HEIGHT * scaleFactor;
429-
430- setLocation((int) positionX, (int) positionY);
431- setSize((int) width, (int) height);
432- }
433-
434- @Override
435- public void paintComponent(Graphics g) {
436- super.paintComponent(g);
437- paintControl(g);
438- }
439-
440- public void showPopupMenu(int x, int y) {
441- JPopupMenu menu = createPopupMenu();
442- menu.show(this, x, y);
443- }
444-
445- protected void moveLabelRelativeToNewPlaceLocation(JComponent component,
446- int newPlaceX, int newPlaceY) {
447- Point componentLocation = component.getLocation();
448- Point placeLocation = getLocation();
449-
450- int componentPlaceDiffX = componentLocation.x - placeLocation.x;
451- int componentPlaceDiffY = componentLocation.y - placeLocation.y;
452-
453- component.setLocation(newPlaceX + componentPlaceDiffX, newPlaceY
454- + componentPlaceDiffY);
455- }
456-
457- protected void selectChildren() {
458- }
459-
460- protected void deselectChildren() {
461- }
462-
463- public void addMouseListeners() {
464- }
465-
466- public void removeMouseListeners() {
467- }
468-
469- protected abstract void paintControl(Graphics g);
470-
471- protected abstract JPopupMenu createPopupMenu();
472-
473- public void removeChildControls() {
474- }
475-
476- public void addChildControls() {
477- }
478-}
479
480=== removed file 'src/dk/aau/cs/gui/components/TextLabel.java'
481--- src/dk/aau/cs/gui/components/TextLabel.java 2011-09-23 21:23:31 +0000
482+++ src/dk/aau/cs/gui/components/TextLabel.java 1970-01-01 00:00:00 +0000
483@@ -1,90 +0,0 @@
484-package dk.aau.cs.gui.components;
485-
486-import java.awt.Component;
487-import java.awt.Font;
488-import java.awt.Point;
489-import java.awt.event.MouseEvent;
490-import java.awt.event.MouseListener;
491-import java.awt.event.MouseMotionListener;
492-import java.awt.event.MouseWheelEvent;
493-import java.awt.event.MouseWheelListener;
494-
495-import javax.swing.JComponent;
496-import javax.swing.JLabel;
497-import javax.swing.event.MouseInputAdapter;
498-
499-import pipe.gui.Pipe;
500-import dk.aau.cs.gui.DrawingSurface;
501-import dk.aau.cs.gui.components.handlers.DragHandler;
502-
503-public class TextLabel extends JLabel {
504- private static final long serialVersionUID = 2836463890383282585L;
505- private JComponent owner;
506- private DrawingSurface drawingSurface;
507-
508- public TextLabel(DrawingSurface drawingSurface, JComponent owner,
509- Point locationRelativeTo, String text) {
510- this.drawingSurface = drawingSurface;
511- this.owner = owner;
512-
513- setFont(new Font(Pipe.LABEL_FONT, Font.BOLD,
514- Pipe.LABEL_DEFAULT_FONT_SIZE));
515- setCursor(new java.awt.Cursor(java.awt.Cursor.CROSSHAIR_CURSOR));
516- setFocusable(false);
517- setOpaque(false);
518- setBackground(Pipe.BACKGROUND_COLOR);
519- setText(text);
520- setLocation(locationRelativeTo.x - getPreferredSize().width,
521- locationRelativeTo.y);
522- updateSize();
523- }
524-
525- public void addMouseListeners() {
526- removeMouseListeners();
527-
528- MouseWheelAndClickPassThroughHandler clickAndWheelHandler = new MouseWheelAndClickPassThroughHandler(
529- owner);
530- addMouseListener(clickAndWheelHandler);
531- addMouseWheelListener(clickAndWheelHandler);
532- addMouseMotionListener(new DragHandler(this, drawingSurface, false));
533- }
534-
535- public void removeMouseListeners() {
536- for (MouseListener listener : getMouseListeners())
537- removeMouseListener(listener);
538- for (MouseWheelListener listener : getMouseWheelListeners())
539- removeMouseWheelListener(listener);
540- for (MouseMotionListener listener : getMouseMotionListeners())
541- removeMouseMotionListener(listener);
542- }
543-
544- private void updateSize() {
545- setSize(getPreferredSize().width, getPreferredSize().height);
546- }
547-
548- public void zoom(int percentage) {
549- float newSize = Pipe.LABEL_DEFAULT_FONT_SIZE * (percentage / 100.0f);
550- Font newFont = getFont().deriveFont(newSize);
551- setFont(newFont);
552- updateSize();
553- }
554-
555- private class MouseWheelAndClickPassThroughHandler extends
556- MouseInputAdapter {
557- private Component targetComponent;
558-
559- public MouseWheelAndClickPassThroughHandler(Component target) {
560- targetComponent = target;
561- }
562-
563- @Override
564- public void mouseClicked(MouseEvent e) {
565- targetComponent.dispatchEvent(e);
566- }
567-
568- @Override
569- public void mouseWheelMoved(MouseWheelEvent e) {
570- targetComponent.dispatchEvent(e);
571- }
572- }
573-}
574
575=== removed file 'src/dk/aau/cs/gui/components/TimedPlaceControl.java'
576--- src/dk/aau/cs/gui/components/TimedPlaceControl.java 2012-10-14 12:07:04 +0000
577+++ src/dk/aau/cs/gui/components/TimedPlaceControl.java 1970-01-01 00:00:00 +0000
578@@ -1,200 +0,0 @@
579-package dk.aau.cs.gui.components;
580-
581-import java.awt.BasicStroke;
582-import java.awt.Color;
583-import java.awt.Graphics;
584-import java.awt.Graphics2D;
585-import java.awt.Point;
586-import java.awt.RenderingHints;
587-import java.awt.event.ActionEvent;
588-import java.awt.event.ActionListener;
589-import java.awt.event.MouseListener;
590-import java.awt.event.MouseMotionListener;
591-import java.awt.geom.Ellipse2D;
592-
593-import javax.swing.BorderFactory;
594-import javax.swing.JMenuItem;
595-import javax.swing.JPopupMenu;
596-
597-import pipe.gui.Pipe;
598-import dk.aau.cs.gui.DrawingSurface;
599-import dk.aau.cs.gui.components.handlers.ClickHandler;
600-import dk.aau.cs.gui.components.handlers.DragHandler;
601-import dk.aau.cs.model.tapn.LocalTimedPlace;
602-
603-public class TimedPlaceControl extends PetriNetElementControl {
604- private static final long serialVersionUID = 3512995997457683903L;
605-
606- private static final float DEFAULT_LINE_THICKNESS = 1.0f;
607- private static final int DRAW_OFFSET = 1;
608-
609- private final LocalTimedPlace timedPlace;
610- private TextLabel nameLabel;
611- private TextLabel invariantLabel;
612-
613- private float lineThickness = DEFAULT_LINE_THICKNESS;
614- private boolean attributesVisible = true;
615-
616- public TimedPlaceControl(DrawingSurface parent, LocalTimedPlace timedPlace,
617- Point position) {
618- super(parent, position);
619- this.timedPlace = timedPlace;
620-
621- setLocation(position);
622- setSize(Pipe.PLACE_TRANSITION_HEIGHT + DRAW_OFFSET,
623- Pipe.PLACE_TRANSITION_HEIGHT + DRAW_OFFSET);
624- this.setBorder(BorderFactory.createLineBorder(Color.red));
625-
626- initComponents();
627- addMouseListeners();
628-
629- }
630-
631- private void initComponents() {
632- Point position = getLocation();
633- nameLabel = new TextLabel(parent(), this, new Point(position.x - 5,
634- position.y), timedPlace.name());
635- invariantLabel = new TextLabel(parent(), this, new Point(
636- position.x - 5, position.y + Pipe.LABEL_DEFAULT_FONT_SIZE + 1),
637- "inv: " + timedPlace.invariant().toString());
638- addChildControls();
639- }
640-
641- @Override
642- public void addMouseListeners() {
643- removeMouseListeners();
644- addMouseMotionListener(new DragHandler(this, parent(), true));
645- addMouseListener(new ClickHandler(this));
646-
647- nameLabel.addMouseListeners();
648- invariantLabel.addMouseListeners();
649- }
650-
651- @Override
652- public void removeMouseListeners() {
653- for (MouseMotionListener listener : getMouseMotionListeners())
654- removeMouseMotionListener(listener);
655- for (MouseListener listener : getMouseListeners())
656- removeMouseListener(listener);
657- nameLabel.removeMouseListeners();
658- invariantLabel.removeMouseListeners();
659- }
660-
661- public boolean isAttributesVisible() {
662- return attributesVisible;
663- }
664-
665- public void setAttributesVisible(boolean value) {
666- if (value != attributesVisible) {
667- attributesVisible = value;
668- if (value) {
669- addChildControls();
670- } else {
671- removeChildControls();
672- }
673- }
674- }
675-
676- @Override
677- public void addChildControls() {
678- parent().add(nameLabel);
679- parent().add(invariantLabel);
680- // parent().surfaceChanged();
681- }
682-
683- @Override
684- public void removeChildControls() {
685- parent().remove(nameLabel);
686- parent().remove(invariantLabel);
687- // parent().surfaceChanged();
688- }
689-
690- @Override
691- public void setLocation(int x, int y) {
692- if (nameLabel != null)
693- moveLabelRelativeToNewPlaceLocation(nameLabel, x, y);
694- if (invariantLabel != null)
695- moveLabelRelativeToNewPlaceLocation(invariantLabel, x, y);
696- super.setLocation(x, y);
697- }
698-
699- @Override
700- public void zoom(int percentage) {
701- super.zoom(percentage);
702- nameLabel.zoom(percentage);
703- invariantLabel.zoom(percentage);
704- lineThickness = DEFAULT_LINE_THICKNESS * (percentage / 100.0f);
705- }
706-
707- @Override
708- protected void selectChildren() {
709- nameLabel.setForeground(Pipe.SELECTION_TEXT_COLOUR);
710- invariantLabel.setForeground(Pipe.SELECTION_TEXT_COLOUR);
711- }
712-
713- @Override
714- protected void deselectChildren() {
715- nameLabel.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
716- invariantLabel.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
717- }
718-
719- @Override
720- protected void paintControl(Graphics g) {
721- Graphics2D g2 = (Graphics2D) g;
722-
723- g2.setStroke(new BasicStroke(lineThickness));
724- g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING,
725- RenderingHints.VALUE_ANTIALIAS_ON);
726-
727- g2.setColor(isSelected() ? Pipe.SELECTION_FILL_COLOUR
728- : Pipe.ELEMENT_FILL_COLOUR);
729- Ellipse2D.Double ellipse = new Ellipse2D.Double(0, 0, getSize().width
730- - DRAW_OFFSET, getSize().height - DRAW_OFFSET);
731- g2.fill(ellipse);
732-
733- g2.setPaint(isSelected() ? Pipe.SELECTION_LINE_COLOUR
734- : Pipe.ELEMENT_LINE_COLOUR);
735- g2.draw(ellipse);
736- }
737-
738- @Override
739- public JPopupMenu createPopupMenu() {
740- JPopupMenu menu = new JPopupMenu();
741-
742- if (attributesVisible) {
743- JMenuItem item = new JMenuItem("Hide Attributes");
744- item.addActionListener(new ActionListener() {
745- public void actionPerformed(ActionEvent arg0) {
746- setAttributesVisible(false);
747- }
748- });
749- menu.add(item);
750- } else {
751- JMenuItem item = new JMenuItem("Show Attributes");
752- item.addActionListener(new ActionListener() {
753- public void actionPerformed(ActionEvent arg0) {
754- setAttributesVisible(true);
755- }
756- });
757- menu.add(item);
758- }
759-
760- JMenuItem deleteItem = new JMenuItem("Delete");
761- deleteItem.addActionListener(new ActionListener() {
762- public void actionPerformed(ActionEvent arg0) {
763- // delete();
764- }
765- });
766- menu.add(deleteItem);
767-
768- JMenuItem propertiesItem = new JMenuItem("Properties");
769- propertiesItem.addActionListener(new ActionListener() {
770- public void actionPerformed(ActionEvent e) {
771- // showEditor();
772- }
773- });
774- menu.add(propertiesItem);
775-
776- return menu;
777- }
778-}
779
780=== removed file 'src/dk/aau/cs/gui/components/handlers/ClickHandler.java'
781--- src/dk/aau/cs/gui/components/handlers/ClickHandler.java 2011-03-02 19:03:58 +0000
782+++ src/dk/aau/cs/gui/components/handlers/ClickHandler.java 1970-01-01 00:00:00 +0000
783@@ -1,34 +0,0 @@
784-package dk.aau.cs.gui.components.handlers;
785-
786-import java.awt.event.MouseEvent;
787-
788-import javax.swing.JOptionPane;
789-import javax.swing.SwingUtilities;
790-import javax.swing.event.MouseInputAdapter;
791-
792-import dk.aau.cs.gui.components.PetriNetElementControl;
793-
794-public class ClickHandler extends MouseInputAdapter {
795- private PetriNetElementControl control;
796-
797- public ClickHandler(PetriNetElementControl control) {
798- this.control = control;
799- }
800-
801- @Override
802- public void mouseClicked(MouseEvent e) {
803- if (SwingUtilities.isLeftMouseButton(e)) {
804- if (e.getClickCount() == 2) {
805- JOptionPane.showMessageDialog(null, "editor");
806- } else {
807- control.select();
808- // JOptionPane.showMessageDialog(null, "select");
809- // if not animation mode
810- // select control
811- }
812- } else if (SwingUtilities.isRightMouseButton(e)) {
813- // if not animation mode
814- control.showPopupMenu(e.getX(), e.getY());
815- }
816- }
817-}
818
819=== removed file 'src/dk/aau/cs/gui/components/handlers/DragHandler.java'
820--- src/dk/aau/cs/gui/components/handlers/DragHandler.java 2011-06-28 16:30:37 +0000
821+++ src/dk/aau/cs/gui/components/handlers/DragHandler.java 1970-01-01 00:00:00 +0000
822@@ -1,50 +0,0 @@
823-package dk.aau.cs.gui.components.handlers;
824-
825-import java.awt.Point;
826-import java.awt.event.MouseEvent;
827-
828-import javax.swing.JComponent;
829-
830-import pipe.gui.Grid;
831-import dk.aau.cs.gui.DrawingSurface;
832-
833-public class DragHandler extends javax.swing.event.MouseInputAdapter {
834- private Point anchorPoint;
835- private JComponent draggableComponent;
836- private DrawingSurface drawingSurface;
837- private boolean snapToGrid;
838-
839- public DragHandler(JComponent draggableComponent,
840- DrawingSurface drawingSurface, boolean snapToGrid) {
841- this.draggableComponent = draggableComponent;
842- this.drawingSurface = drawingSurface;
843- this.snapToGrid = snapToGrid;
844- }
845-
846- @Override
847- public void mouseMoved(MouseEvent e) {
848- anchorPoint = e.getPoint();
849- }
850-
851- @Override
852- public void mouseDragged(MouseEvent e) {
853- int anchorX = anchorPoint.x;
854- int anchorY = anchorPoint.y;
855-
856- Point parentOnScreen = draggableComponent.getParent().getLocationOnScreen();
857- Point mouseOnScreen = e.getLocationOnScreen();
858-
859- int x = Math.max(0, mouseOnScreen.x - parentOnScreen.x - anchorX);
860- int y = Math.max(0, mouseOnScreen.y - parentOnScreen.y - anchorY);
861-
862- if (snapToGrid) {
863- x = Grid.getModifiedX(x);
864- y = Grid.getModifiedY(y);
865- }
866-
867- Point position = new Point(x, y);
868- draggableComponent.setLocation(position);
869-
870- drawingSurface.updatePreferredSize();
871- }
872-}
873\ No newline at end of file
874
875=== removed file 'src/dk/aau/cs/gui/undo/AddPetriNetControlCommand.java'
876--- src/dk/aau/cs/gui/undo/AddPetriNetControlCommand.java 2011-03-02 19:03:58 +0000
877+++ src/dk/aau/cs/gui/undo/AddPetriNetControlCommand.java 1970-01-01 00:00:00 +0000
878@@ -1,29 +0,0 @@
879-package dk.aau.cs.gui.undo;
880-
881-import dk.aau.cs.gui.DrawingSurface;
882-import dk.aau.cs.gui.components.PetriNetElementControl;
883-
884-public class AddPetriNetControlCommand extends Command {
885- private PetriNetElementControl control;
886- private DrawingSurface surface;
887-
888- public AddPetriNetControlCommand(PetriNetElementControl control,
889- DrawingSurface surface) {
890- this.surface = surface;
891- this.control = control;
892- }
893-
894- @Override
895- public void redo() {
896- control.addChildControls();
897- surface.add(control);
898- // surface.surfaceChanged();
899- }
900-
901- @Override
902- public void undo() {
903- control.removeChildControls();
904- surface.remove(control);
905- // surface.surfaceChanged();
906- }
907-}
908
909=== modified file 'src/dk/aau/cs/io/TraceImportExport.java'
910--- src/dk/aau/cs/io/TraceImportExport.java 2014-08-04 21:06:50 +0000
911+++ src/dk/aau/cs/io/TraceImportExport.java 2018-07-04 11:38:47 +0000
912@@ -13,7 +13,7 @@
913 import org.w3c.dom.Document;
914 import org.w3c.dom.Element;
915 import javax.swing.JOptionPane;
916-import pipe.gui.widgets.FileBrowser;
917+import pipe.gui.widgets.filebrowser.FileBrowser;
918 import dk.aau.cs.model.tapn.TimedArcPetriNet;
919 import dk.aau.cs.model.tapn.TimedToken;
920 import dk.aau.cs.model.tapn.TimedTransition;
921@@ -47,9 +47,9 @@
922 try {
923 ByteArrayOutputStream os = prepareTraceStream();
924
925- FileBrowser fb = new FileBrowser("Export Trace", "trc");
926+ FileBrowser fb = FileBrowser.constructor("Export Trace", "trc");
927 // path = fb.saveFile(CreateGui.appGui.getCurrentTabName().substring(0, CreateGui.appGui.getCurrentTabName().lastIndexOf('.')) + "-trace");
928- path = fb.saveFile(CreateGui.appGui.getCurrentTabName().substring(0, CreateGui.appGui.getCurrentTabName().lastIndexOf('.')));
929+ path = fb.saveFile(CreateGui.getAppGui().getCurrentTabName().substring(0, CreateGui.getAppGui().getCurrentTabName().lastIndexOf('.')));
930
931 FileOutputStream fs = new FileOutputStream(path);
932 fs.write(os.toByteArray());
933@@ -148,7 +148,7 @@
934 }
935
936 public static void importTrace() {
937- if (pipe.gui.CreateGui.getAnimationHistory().getListModel().size() > 1) {
938+ if (pipe.gui.CreateGui.getCurrentTab().getAnimationHistory().getListModel().size() > 1) {
939 int answer = JOptionPane.showConfirmDialog(CreateGui.getApp(),
940 "You are about to import a trace. This removes the current trace.",
941 "Import Trace", JOptionPane.OK_CANCEL_OPTION, JOptionPane.WARNING_MESSAGE);
942@@ -157,7 +157,7 @@
943 }
944 }
945
946- FileBrowser fb = new FileBrowser("Import Trace", "trc");
947+ FileBrowser fb = FileBrowser.constructor ("Import Trace", "trc");
948 File f = fb.openFile();
949
950 if (f == null) {
951
952=== added file 'src/dk/aau/cs/util/JavaUtil.java'
953--- src/dk/aau/cs/util/JavaUtil.java 1970-01-01 00:00:00 +0000
954+++ src/dk/aau/cs/util/JavaUtil.java 2018-07-04 11:38:47 +0000
955@@ -0,0 +1,23 @@
956+package dk.aau.cs.util;
957+
958+import dk.aau.cs.debug.Logger;
959+
960+public class JavaUtil {
961+ public static int getJREMajorVersion(){
962+ String version = System.getProperty("java.version");
963+ String[] versionSplit = version.split("\\.");
964+
965+ try {
966+ if (Integer.parseInt(versionSplit[0]) >= 9) {
967+ //Version format (9.X.Y)
968+ return Integer.parseInt(versionSplit[0]);
969+ } else {
970+ //Before java 9 version in format (1.X.Y)
971+ return Integer.parseInt(versionSplit[1]);
972+ }
973+ } catch (NumberFormatException e) {
974+ Logger.log("Error parsing java version, failing silent (0): " + e.getMessage());
975+ return 0; // Unknown version
976+ }
977+ }
978+}
979
980=== modified file 'src/dk/aau/cs/util/Require.java'
981--- src/dk/aau/cs/util/Require.java 2011-03-07 18:40:05 +0000
982+++ src/dk/aau/cs/util/Require.java 2018-07-04 11:38:47 +0000
983@@ -6,6 +6,11 @@
984 throw new RequireException(message);
985 }
986
987+ public static void notNull(Object o, String message) {
988+ if (o == null)
989+ throw new RequireException(message);
990+ }
991+
992 public static void notImplemented(){
993 throw new RuntimeException("NOT IMPLEMENTED");
994 }
995
996=== modified file 'src/dk/aau/cs/verification/UPPAAL/Verifyta.java'
997--- src/dk/aau/cs/verification/UPPAAL/Verifyta.java 2014-03-06 05:43:24 +0000
998+++ src/dk/aau/cs/verification/UPPAAL/Verifyta.java 2018-07-04 11:38:47 +0000
999@@ -10,10 +10,8 @@
1000 import java.util.regex.Pattern;
1001
1002 import net.tapaal.Preferences;
1003-import pipe.dataLayer.TAPNQuery.SearchOption;
1004 import pipe.dataLayer.TAPNQuery.TraceOption;
1005 import pipe.gui.FileFinder;
1006-import pipe.gui.FileFinderImpl;
1007 import pipe.gui.MessengerImpl;
1008 import pipe.gui.Pipe;
1009 import dk.aau.cs.Messenger;
1010@@ -28,7 +26,6 @@
1011 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
1012 import dk.aau.cs.translations.ReductionOption;
1013 import dk.aau.cs.util.ExecutabilityChecker;
1014-import dk.aau.cs.util.MemoryMonitor;
1015 import dk.aau.cs.util.Tuple;
1016 import dk.aau.cs.util.UnsupportedModelException;
1017 import dk.aau.cs.util.UnsupportedQueryException;
1018@@ -36,7 +33,6 @@
1019 import dk.aau.cs.verification.NameMapping;
1020 import dk.aau.cs.verification.ProcessRunner;
1021 import dk.aau.cs.verification.QueryResult;
1022-import dk.aau.cs.verification.QueryType;
1023 import dk.aau.cs.verification.VerificationOptions;
1024 import dk.aau.cs.verification.VerificationResult;
1025
1026@@ -186,7 +182,7 @@
1027 if (verifyta != null && !verifyta.equals("")) {
1028 if (new File(verifyta).exists()){
1029 verifytapath = verifyta;
1030- Verifyta v = new Verifyta(new FileFinderImpl(), new MessengerImpl());
1031+ Verifyta v = new Verifyta(new FileFinder(), new MessengerImpl());
1032 if(v.isCorrectVersion()){
1033 return true;
1034 }else{
1035@@ -199,7 +195,7 @@
1036 verifyta = Preferences.getInstance().getVerifytaLocation();
1037 if (verifyta != null && !verifyta.equals("")) {
1038 verifytapath = verifyta;
1039- Verifyta v = new Verifyta(new FileFinderImpl(), new MessengerImpl());
1040+ Verifyta v = new Verifyta(new FileFinder(), new MessengerImpl());
1041 if(v.isCorrectVersion()){
1042 return true;
1043 }else{
1044
1045=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
1046--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2017-06-27 13:49:24 +0000
1047+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2018-07-04 11:38:47 +0000
1048@@ -17,15 +17,12 @@
1049 import pipe.dataLayer.TAPNQuery.SearchOption;
1050 import pipe.dataLayer.TAPNQuery.TraceOption;
1051 import pipe.gui.FileFinder;
1052-import pipe.gui.FileFinderImpl;
1053 import pipe.gui.MessengerImpl;
1054 import pipe.gui.Pipe;
1055 import pipe.gui.widgets.InclusionPlaces;
1056 import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
1057 import dk.aau.cs.Messenger;
1058 import dk.aau.cs.TCTL.TCTLAFNode;
1059-import dk.aau.cs.TCTL.TCTLAGNode;
1060-import dk.aau.cs.TCTL.TCTLEFNode;
1061 import dk.aau.cs.TCTL.TCTLEGNode;
1062 import dk.aau.cs.model.tapn.LocalTimedPlace;
1063 import dk.aau.cs.model.tapn.TAPNQuery;
1064@@ -40,7 +37,6 @@
1065 import dk.aau.cs.verification.NameMapping;
1066 import dk.aau.cs.verification.ProcessRunner;
1067 import dk.aau.cs.verification.QueryResult;
1068-import dk.aau.cs.verification.QueryType;
1069 import dk.aau.cs.verification.Stats;
1070 import dk.aau.cs.verification.VerificationOptions;
1071 import dk.aau.cs.verification.VerificationResult;
1072@@ -227,7 +223,7 @@
1073 if (verifypn != null && !verifypn.isEmpty()) {
1074 if (new File(verifypn).exists()){
1075 verifypnpath = verifypn;
1076- VerifyPN v = new VerifyPN(new FileFinderImpl(), new MessengerImpl());
1077+ VerifyPN v = new VerifyPN(new FileFinder(), new MessengerImpl());
1078 if(v.isCorrectVersion()){
1079 return true;
1080 }else{
1081@@ -254,7 +250,7 @@
1082 if (verifypnfile.exists()){
1083
1084 verifypnpath = verifypnfile.getAbsolutePath();
1085- VerifyPN v = new VerifyPN(new FileFinderImpl(), new MessengerImpl());
1086+ VerifyPN v = new VerifyPN(new FileFinder(), new MessengerImpl());
1087 if(v.isCorrectVersion()){
1088 return true;
1089 }else{
1090
1091=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
1092--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2014-05-09 16:52:21 +0000
1093+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2018-07-04 11:38:47 +0000
1094@@ -15,7 +15,6 @@
1095 import net.tapaal.TAPAAL;
1096 import pipe.dataLayer.TAPNQuery.TraceOption;
1097 import pipe.gui.FileFinder;
1098-import pipe.gui.FileFinderImpl;
1099 import pipe.gui.MessengerImpl;
1100 import pipe.gui.Pipe;
1101 import pipe.gui.widgets.InclusionPlaces;
1102@@ -38,7 +37,6 @@
1103 import dk.aau.cs.verification.NameMapping;
1104 import dk.aau.cs.verification.ProcessRunner;
1105 import dk.aau.cs.verification.QueryResult;
1106-import dk.aau.cs.verification.QueryType;
1107 import dk.aau.cs.verification.Stats;
1108 import dk.aau.cs.verification.VerificationOptions;
1109 import dk.aau.cs.verification.VerificationResult;
1110@@ -215,7 +213,7 @@
1111 if (verifytapn != null && !verifytapn.isEmpty()) {
1112 if (new File(verifytapn).exists()){
1113 verifytapnpath = verifytapn;
1114- VerifyTAPN v = new VerifyTAPN(new FileFinderImpl(), new MessengerImpl());
1115+ VerifyTAPN v = new VerifyTAPN(new FileFinder(), new MessengerImpl());
1116 if(v.isCorrectVersion()){
1117 return true;
1118 }else{
1119@@ -242,7 +240,7 @@
1120 if (verifytapnfile.exists()){
1121
1122 verifytapnpath = verifytapnfile.getAbsolutePath();
1123- VerifyTAPN v = new VerifyTAPN(new FileFinderImpl(), new MessengerImpl());
1124+ VerifyTAPN v = new VerifyTAPN(new FileFinder(), new MessengerImpl());
1125 if(v.isCorrectVersion()){
1126 return true;
1127 }else{
1128
1129=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
1130--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2014-06-13 22:38:04 +0000
1131+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2018-07-04 11:38:47 +0000
1132@@ -36,7 +36,6 @@
1133 import pipe.dataLayer.TAPNQuery.TraceOption;
1134 import pipe.dataLayer.TAPNQuery.WorkflowMode;
1135 import pipe.gui.FileFinder;
1136-import pipe.gui.FileFinderImpl;
1137 import pipe.gui.MessengerImpl;
1138 import pipe.gui.Pipe;
1139 import pipe.gui.widgets.InclusionPlaces;
1140@@ -216,7 +215,7 @@
1141 if (verifydtapn != null && !verifydtapn.isEmpty()) {
1142 if (new File(verifydtapn).exists()){
1143 verifydtapnpath = verifydtapn;
1144- VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinderImpl(), new MessengerImpl());
1145+ VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
1146 if(v.isCorrectVersion()){
1147 return true;
1148 }else{
1149@@ -243,7 +242,7 @@
1150 if (verifydtapnfile.exists()){
1151
1152 verifydtapnpath = verifydtapnfile.getAbsolutePath();
1153- VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinderImpl(), new MessengerImpl());
1154+ VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
1155 if(v.isCorrectVersion()){
1156 return true;
1157 }else{
1158
1159=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
1160--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2018-04-02 20:03:24 +0000
1161+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2018-07-04 11:38:47 +0000
1162@@ -9,7 +9,7 @@
1163 import pipe.dataLayer.TAPNQuery.SearchOption;
1164 import pipe.dataLayer.TAPNQuery.TraceOption;
1165 import pipe.gui.CreateGui;
1166-import pipe.gui.FileFinderImpl;
1167+import pipe.gui.FileFinder;
1168 import pipe.gui.MessengerImpl;
1169 import pipe.gui.widgets.QueryPane;
1170 import dk.aau.cs.Messenger;
1171@@ -377,7 +377,7 @@
1172 BatchProcessingVerificationResult result;
1173 if(QueryPane.getTemporaryFile() != null && fileName.equals(QueryPane.getTemporaryFile().getName())) {
1174 //removes numbers from tempFile so it looks good
1175- result = new BatchProcessingVerificationResult(CreateGui.appGui.getCurrentTabName(), query, verificationResult, verificationTime, MemoryMonitor.getPeakMemory(), stats);
1176+ result = new BatchProcessingVerificationResult(CreateGui.getAppGui().getCurrentTabName(), query, verificationResult, verificationTime, MemoryMonitor.getPeakMemory(), stats);
1177 } else {
1178 result = new BatchProcessingVerificationResult(fileName, query, verificationResult, verificationTime, MemoryMonitor.getPeakMemory(), stats);
1179 }
1180@@ -465,25 +465,25 @@
1181 }
1182
1183 private Verifyta getVerifyta() {
1184- Verifyta verifyta = new Verifyta(new FileFinderImpl(), new MessengerImpl());
1185+ Verifyta verifyta = new Verifyta(new FileFinder(), new MessengerImpl());
1186 verifyta.setup();
1187 return verifyta;
1188 }
1189
1190 private static VerifyTAPN getVerifyTAPN() {
1191- VerifyTAPN verifytapn = new VerifyTAPN(new FileFinderImpl(), new MessengerImpl());
1192+ VerifyTAPN verifytapn = new VerifyTAPN(new FileFinder(), new MessengerImpl());
1193 verifytapn.setup();
1194 return verifytapn;
1195 }
1196
1197 private static VerifyPN getVerifyPN() {
1198- VerifyPN verifypn = new VerifyPN(new FileFinderImpl(), new MessengerImpl());
1199+ VerifyPN verifypn = new VerifyPN(new FileFinder(), new MessengerImpl());
1200 verifypn.setup();
1201 return verifypn;
1202 }
1203
1204 private static VerifyTAPNDiscreteVerification getVerifyTAPNDiscreteVerification() {
1205- VerifyTAPNDiscreteVerification verifytapnDiscreteVerification = new VerifyTAPNDiscreteVerification(new FileFinderImpl(), new MessengerImpl());
1206+ VerifyTAPNDiscreteVerification verifytapnDiscreteVerification = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
1207 verifytapnDiscreteVerification.setup();
1208 return verifytapnDiscreteVerification;
1209 }
1210
1211=== modified file 'src/net/tapaal/TAPAAL.java'
1212--- src/net/tapaal/TAPAAL.java 2014-02-08 16:38:01 +0000
1213+++ src/net/tapaal/TAPAAL.java 2018-07-04 11:38:47 +0000
1214@@ -45,7 +45,7 @@
1215 try {
1216 commandline = parser.parse(options, args);
1217 } catch (ParseException exp) {
1218- System.err.println("There where an error parsing the specifyed arguments");
1219+ System.err.println("There where an error parsing the specified arguments");
1220 System.err.println("Unexpected exception:" + exp.getMessage());
1221 }
1222
1223@@ -57,6 +57,11 @@
1224 Logger.enableLogging(true);
1225 }
1226
1227+ if (TAPAAL.VERSION == "DEV"){
1228+ Logger.enableLogging(true);
1229+ Logger.log("Debug logging is enabled by default in DEV branch");
1230+ }
1231+
1232 // Open files
1233 String[] files = commandline.getArgs();
1234 for (String f : files) {
1235@@ -64,7 +69,7 @@
1236
1237 if (file.exists()) { // Open the file
1238 if (file.canRead()) {
1239- CreateGui.appGui.createNewTabFromFile(file, false);
1240+ CreateGui.getAppGui().createNewTabFromFile(file);
1241 } else if (file.exists()) {
1242 System.err.println("Can not read file " + file.toString());
1243 }
1244
1245=== modified file 'src/pipe/dataLayer/DataLayer.java'
1246--- src/pipe/dataLayer/DataLayer.java 2014-02-27 13:04:19 +0000
1247+++ src/pipe/dataLayer/DataLayer.java 2018-07-04 11:38:47 +0000
1248@@ -72,14 +72,6 @@
1249 * Create empty Petri-Net object
1250 */
1251 public DataLayer() {
1252- initializeMatrices();
1253- }
1254-
1255- /**
1256- * Initialize Arrays
1257- */
1258- private void initializeMatrices() {
1259-
1260 placesArray = new ArrayList<Place>();
1261 transitionsArray = new ArrayList<Transition>();
1262 arcsArray = new ArrayList<Arc>();
1263@@ -92,6 +84,7 @@
1264 tapnInhibitorsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>>();
1265 }
1266
1267+
1268 /**
1269 * Add placeInput to the back of the Place ArrayList All observers are
1270 * notified of this change (Model-View Architecture)
1271
1272=== modified file 'src/pipe/dataLayer/Template.java'
1273--- src/pipe/dataLayer/Template.java 2012-01-27 10:21:31 +0000
1274+++ src/pipe/dataLayer/Template.java 2018-07-04 11:38:47 +0000
1275@@ -37,7 +37,7 @@
1276 }
1277
1278 public void setGuiModel(DataLayer guiModel) {
1279- Require.that(guiModel != null, "GuiModel cannot be null");
1280+ Require.notNull(guiModel, "GuiModel cannot be null");
1281 this.guiModel = guiModel;
1282 }
1283
1284
1285=== modified file 'src/pipe/gui/AnimationController.java'
1286--- src/pipe/gui/AnimationController.java 2014-11-05 14:20:41 +0000
1287+++ src/pipe/gui/AnimationController.java 2018-07-04 11:38:47 +0000
1288@@ -29,24 +29,17 @@
1289 import javax.swing.JTextField;
1290 import javax.swing.JToggleButton;
1291 import javax.swing.JToolBar;
1292-import javax.swing.KeyStroke;
1293 import javax.swing.ToolTipManager;
1294 import javax.swing.border.EmptyBorder;
1295 import javax.swing.text.AbstractDocument;
1296-import javax.swing.text.AttributeSet;
1297-import javax.swing.text.BadLocationException;
1298-import javax.swing.text.DocumentFilter;
1299-import javax.swing.text.DocumentFilter.FilterBypass;
1300+
1301 import pipe.dataLayer.NetType;
1302-import pipe.gui.GuiFrame.AnimateAction;
1303-import pipe.gui.Pipe.ElementType;
1304 import pipe.gui.action.GuiAction;
1305 import pipe.gui.widgets.DecimalOnlyDocumentFilter;
1306 import dk.aau.cs.gui.components.NonsearchableJComboBox;
1307 import dk.aau.cs.model.tapn.simulation.FiringMode;
1308-import java.awt.BorderLayout;
1309+
1310 import java.awt.event.ActionListener;
1311-import java.util.Dictionary;
1312 import java.util.Hashtable;
1313 import javax.swing.JButton;
1314 import javax.swing.JSlider;
1315@@ -64,72 +57,27 @@
1316
1317 public class AnimationController extends JPanel {
1318
1319- /**
1320- *
1321- */
1322 private static final long serialVersionUID = 7037756165634426275L;
1323 private javax.swing.JButton okButton;
1324- private JSlider delaySlider;
1325- private int delayScale = 10;
1326- private String PRECISION_ERROR_MESSAGE = "The precision is limited to 5 decimal places, the number will be truncated.";
1327- private String PRECISION_ERROR_DIALOG_TITLE = "Precision of Time Delay Exceeded";
1328-
1329- class ToggleButton extends JToggleButton implements PropertyChangeListener {
1330-
1331- /**
1332- *
1333- */
1334- private static final long serialVersionUID = -6594894202788511816L;
1335-
1336- public ToggleButton(Action a) {
1337- super(a);
1338- if (a.getValue(Action.SMALL_ICON) != null) {
1339- // toggle buttons like to have images *and* text, nasty
1340- setText(null);
1341- }
1342- a.addPropertyChangeListener(this);
1343- }
1344-
1345- public void propertyChange(PropertyChangeEvent evt) {
1346- if (evt.getPropertyName().equals("selected")) {
1347- Boolean b = (Boolean) evt.getNewValue();
1348- if (b != null) {
1349- setSelected(b.booleanValue());
1350- }
1351- }
1352- }
1353-
1354- }
1355-
1356- private void addButton(JToolBar toolBar, GuiAction action) {
1357-
1358- if (action.getValue("selected") != null) {
1359- toolBar.add(new ToggleButton(action));
1360- } else {
1361- toolBar.add(action);
1362- }
1363- }
1364-
1365- AnimateAction startAction, stepforwardAction, stepbackwardAction,
1366- randomAction, randomAnimateAction, timeAction;
1367+ private JSlider delaySlider;
1368+ private int delayScale = 10;
1369+ private static final String PRECISION_ERROR_MESSAGE = "The precision is limited to 5 decimal places, the number will be truncated.";
1370+ private static final String PRECISION_ERROR_DIALOG_TITLE = "Precision of Time Delay Exceeded";
1371+
1372+ private GuiAction stepforwardAction, stepbackwardAction;
1373+
1374+ JTextField TimeDelayField = new JTextField();
1375+ JComboBox firermodebox = null;
1376+ private static final String[] FIRINGMODES = { "Random", "Oldest", "Youngest", "Manual" };
1377
1378 public AnimationController(NetType netType) {
1379- startAction = CreateGui.appGui.startAction;
1380
1381- stepbackwardAction = CreateGui.appGui.stepbackwardAction;
1382- stepforwardAction = CreateGui.appGui.stepforwardAction;
1383+ stepbackwardAction = CreateGui.getAppGui().stepbackwardAction;
1384+ stepforwardAction = CreateGui.getAppGui().stepforwardAction;
1385
1386 stepbackwardAction.setEnabled(false);
1387 stepforwardAction.setEnabled(false);
1388
1389- // timeAction = new AnimateAction("Time", Pipe.TIMEPASS,
1390- // "Let Time pass", "_");
1391-
1392- //randomAction = new AnimateAction("Random", ElementType.RANDOM,
1393- // "Randomly fire a transition", "typed 5");
1394- //randomAnimateAction = new AnimateAction("Simulate", ElementType.ANIMATE,
1395- // "Randomly fire a number of transitions", "typed 7", true);
1396-
1397 setLayout(new GridBagLayout());
1398 GridBagConstraints c = new GridBagConstraints();
1399
1400@@ -149,8 +97,8 @@
1401 JToolBar animationToolBar = new JToolBar();
1402 animationToolBar.setFloatable(false);
1403 animationToolBar.setBorder(new EmptyBorder(0, 0, 0, 0));
1404- addButton(animationToolBar, stepbackwardAction);
1405- addButton(animationToolBar, stepforwardAction);
1406+ animationToolBar.add(stepbackwardAction);
1407+ animationToolBar.add(stepforwardAction);
1408
1409 animationToolBar.setVisible(true);
1410
1411@@ -173,9 +121,9 @@
1412 c.gridy = 0;
1413 add(firemode, c);
1414
1415- initDelayTimePanel(animationToolBar);
1416-
1417- initDelaySlider();
1418+ initDelayTimePanel(animationToolBar);
1419+
1420+ initDelaySlider();
1421 }
1422
1423 setBorder(BorderFactory.createCompoundBorder(BorderFactory
1424@@ -186,168 +134,159 @@
1425
1426 initializeDocumentFilterForDelayInput();
1427 }
1428-
1429- private void initDelaySlider() {
1430- JPanel sliderPanel = new JPanel(new FlowLayout(FlowLayout.CENTER));
1431- JButton decrese = new JButton("-");
1432- decrese.setPreferredSize(new Dimension(20, 30));
1433- decrese.addActionListener(new ActionListener() {
1434- public void actionPerformed(ActionEvent e) {
1435- setDelayModeScale(delayScale / 2);
1436- delaySlider.setValue(delaySlider.getValue() * 2);
1437- }
1438- });
1439- sliderPanel.add(decrese);
1440-
1441- delaySlider = new JSlider(0, 160);
1442- delaySlider.setSnapToTicks(false);
1443- delaySlider.setMajorTickSpacing(10);
1444- delaySlider.setMinorTickSpacing(0);
1445- delaySlider.setPaintLabels(true);
1446- delaySlider.setPaintTicks(true);
1447- delaySlider.addChangeListener(new ChangeListener() {
1448- @Override
1449- public void stateChanged(ChangeEvent e) {
1450- TimeDelayField.setText(Double.toString(delaySlider.getValue() * ((double) delayScale) / 160));
1451- CreateGui.getAnimator().reportBlockingPlaces();
1452-
1453- }
1454- });
1455-
1456- delaySlider.addKeyListener(new KeyListener() {
1457- public void keyPressed(KeyEvent e) {
1458- if (e.getKeyCode() == KeyEvent.VK_ENTER) {
1459- addTimeDelayToHistory();
1460- }
1461- }
1462-
1463- public void keyReleased(KeyEvent e) {
1464- CreateGui.getAnimator().reportBlockingPlaces();
1465- }
1466-
1467- public void keyTyped(KeyEvent e) {
1468-
1469- }
1470- });
1471-
1472- setDelayModeScale(16);
1473-
1474- sliderPanel.add(delaySlider);
1475- JButton increse = new JButton("+");
1476- increse.setPreferredSize(new Dimension(20, 30));
1477- increse.addActionListener(new ActionListener() {
1478- public void actionPerformed(ActionEvent e) {
1479- setDelayModeScale(delayScale * 2);
1480- delaySlider.setValue(delaySlider.getValue() / 2);
1481- }
1482- });
1483- sliderPanel.add(increse);
1484-
1485- GridBagConstraints c = new GridBagConstraints();
1486- c.fill = GridBagConstraints.HORIZONTAL;
1487- c.weightx = 0.5;
1488- c.gridx = 0;
1489- c.gridy = 1;
1490- add(sliderPanel, c);
1491- }
1492-
1493- private void setDelayModeScale(int scale){
1494- if (scale == 0) return;
1495- delayScale = scale;
1496- Hashtable<Integer, JLabel> labels = new Hashtable<Integer, JLabel>();
1497- labels.put(0, new JLabel("0"));
1498- labels.put(160, new JLabel(Integer.toString(delayScale)));
1499- delaySlider.setLabelTable(labels);
1500- }
1501-
1502-
1503- private void initDelayTimePanel(JToolBar animationToolBar) {
1504- JPanel timedelayPanel = new JPanel(new FlowLayout(FlowLayout.LEFT));
1505-
1506- okButton = new javax.swing.JButton();
1507-
1508- okButton.setText("Time delay");
1509- // okButton.setMaximumSize(new java.awt.Dimension(75, 25));
1510- okButton.setMinimumSize(new java.awt.Dimension(75, 25));
1511- // okButton.setPreferredSize(new java.awt.Dimension(75, 25));
1512- okButton.addActionListener(new java.awt.event.ActionListener() {
1513- public void actionPerformed(java.awt.event.ActionEvent evt) {
1514- // okButtonHandler(evt);
1515- addTimeDelayToHistory();
1516- }
1517- });
1518-
1519- //"Hack" to make sure the toolTip for this button is showed as long as possible
1520- okButton.addMouseListener(new MouseAdapter() {
1521- final int defaultDismissTimeout = ToolTipManager.sharedInstance().getDismissDelay();
1522- final int defaultInitalDelay = ToolTipManager.sharedInstance().getInitialDelay();
1523- final int defaultReshowDelay = ToolTipManager.sharedInstance().getReshowDelay();
1524- final int dismissDelayMinutes = Integer.MAX_VALUE;
1525-
1526- @Override
1527- public void mouseEntered(MouseEvent e) {
1528- ToolTipManager.sharedInstance().setDismissDelay(dismissDelayMinutes);
1529- ToolTipManager.sharedInstance().setInitialDelay(0);
1530- ToolTipManager.sharedInstance().setReshowDelay(0);
1531- ToolTipManager.sharedInstance().setEnabled(true);
1532- }
1533-
1534- @Override
1535- public void mouseExited(MouseEvent e) {
1536- ToolTipManager.sharedInstance().setDismissDelay(defaultDismissTimeout);
1537- ToolTipManager.sharedInstance().setInitialDelay(defaultInitalDelay);
1538- ToolTipManager.sharedInstance().setReshowDelay(defaultReshowDelay);
1539- ToolTipManager.sharedInstance().setEnabled(CreateGui.getApp().isShowingToolTips());
1540- }
1541- });
1542-
1543- TimeDelayField.addKeyListener(new KeyListener() {
1544- public void keyPressed(KeyEvent e) {
1545- if (e.getKeyCode() == KeyEvent.VK_ENTER) {
1546- addTimeDelayToHistory();
1547- TimeDelayField.getFocusCycleRootAncestor().requestFocus(); // Remove focus
1548- }
1549- }
1550-
1551- public void keyReleased(KeyEvent e) {
1552- CreateGui.getAnimator().reportBlockingPlaces();
1553- }
1554-
1555- public void keyTyped(KeyEvent e) {
1556-
1557- }
1558-
1559- });
1560-
1561- // Disable shortcuts when focused
1562- TimeDelayField.addFocusListener(new FocusListener() {
1563- public void focusLost(FocusEvent arg0) {
1564- CreateGui.getApp().setStepShotcutEnabled(true);
1565- }
1566-
1567- public void focusGained(FocusEvent arg0) {
1568- CreateGui.getApp().setStepShotcutEnabled(false);
1569- }
1570- });
1571-
1572- DecimalFormat df = new DecimalFormat();
1573- df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
1574- df.setMinimumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
1575-
1576- TimeDelayField.setText(df.format(1f));
1577- TimeDelayField.setColumns(6);
1578-
1579- timedelayPanel.add(TimeDelayField);
1580- timedelayPanel.add(okButton);
1581- //CreateGui.getAnimator().reportBlockingPlaces();
1582-
1583- // c.fill = GridBagConstraints.HORIZONTAL;
1584- // c.weightx = 0.5;
1585- // c.gridx = 0;
1586- // c.gridy = 3;
1587- // add(timedelayPanel, c);
1588- animationToolBar.add(timedelayPanel);
1589- }
1590+
1591+ private void initDelaySlider() {
1592+ JPanel sliderPanel = new JPanel(new FlowLayout(FlowLayout.CENTER));
1593+ JButton decrese = new JButton("-");
1594+ decrese.setPreferredSize(new Dimension(20, 30));
1595+ decrese.addActionListener(new ActionListener() {
1596+ public void actionPerformed(ActionEvent e) {
1597+ setDelayModeScale(delayScale / 2);
1598+ delaySlider.setValue(delaySlider.getValue() * 2);
1599+ }
1600+ });
1601+ sliderPanel.add(decrese);
1602+
1603+ delaySlider = new JSlider(0, 160);
1604+ delaySlider.setSnapToTicks(false);
1605+ delaySlider.setMajorTickSpacing(10);
1606+ delaySlider.setMinorTickSpacing(0);
1607+ delaySlider.setPaintLabels(true);
1608+ delaySlider.setPaintTicks(true);
1609+ delaySlider.addChangeListener(new ChangeListener() {
1610+ @Override
1611+ public void stateChanged(ChangeEvent e) {
1612+ TimeDelayField.setText(Double.toString(delaySlider.getValue() * ((double) delayScale) / 160));
1613+ CreateGui.getAnimator().reportBlockingPlaces();
1614+
1615+ }
1616+ });
1617+
1618+ delaySlider.addKeyListener(new KeyListener() {
1619+ public void keyPressed(KeyEvent e) {
1620+ if (e.getKeyCode() == KeyEvent.VK_ENTER) {
1621+ addTimeDelayToHistory();
1622+ }
1623+ }
1624+
1625+ public void keyReleased(KeyEvent e) {
1626+ CreateGui.getAnimator().reportBlockingPlaces();
1627+ }
1628+
1629+ public void keyTyped(KeyEvent e) {
1630+
1631+ }
1632+ });
1633+
1634+ setDelayModeScale(16);
1635+
1636+ sliderPanel.add(delaySlider);
1637+ JButton increse = new JButton("+");
1638+ increse.setPreferredSize(new Dimension(20, 30));
1639+ increse.addActionListener(new ActionListener() {
1640+ public void actionPerformed(ActionEvent e) {
1641+ setDelayModeScale(delayScale * 2);
1642+ delaySlider.setValue(delaySlider.getValue() / 2);
1643+ }
1644+ });
1645+ sliderPanel.add(increse);
1646+
1647+ GridBagConstraints c = new GridBagConstraints();
1648+ c.fill = GridBagConstraints.HORIZONTAL;
1649+ c.weightx = 0.5;
1650+ c.gridx = 0;
1651+ c.gridy = 1;
1652+ add(sliderPanel, c);
1653+ }
1654+
1655+ private void setDelayModeScale(int scale) {
1656+ if (scale == 0) return;
1657+ delayScale = scale;
1658+ Hashtable<Integer, JLabel> labels = new Hashtable<Integer, JLabel>();
1659+ labels.put(0, new JLabel("0"));
1660+ labels.put(160, new JLabel(Integer.toString(delayScale)));
1661+ delaySlider.setLabelTable(labels);
1662+ }
1663+
1664+
1665+ private void initDelayTimePanel(JToolBar animationToolBar) {
1666+ JPanel timedelayPanel = new JPanel(new FlowLayout(FlowLayout.LEFT));
1667+
1668+ okButton = new javax.swing.JButton();
1669+
1670+ okButton.setText("Time delay");
1671+ okButton.setMinimumSize(new java.awt.Dimension(75, 25));
1672+ okButton.addActionListener(new java.awt.event.ActionListener() {
1673+ public void actionPerformed(java.awt.event.ActionEvent evt) {
1674+ addTimeDelayToHistory();
1675+ }
1676+ });
1677+
1678+ //"Hack" to make sure the toolTip for this button is showed as long as possible
1679+ okButton.addMouseListener(new MouseAdapter() {
1680+ final int defaultDismissTimeout = ToolTipManager.sharedInstance().getDismissDelay();
1681+ final int defaultInitalDelay = ToolTipManager.sharedInstance().getInitialDelay();
1682+ final int defaultReshowDelay = ToolTipManager.sharedInstance().getReshowDelay();
1683+ final int dismissDelayMinutes = Integer.MAX_VALUE;
1684+
1685+ @Override
1686+ public void mouseEntered(MouseEvent e) {
1687+ ToolTipManager.sharedInstance().setDismissDelay(dismissDelayMinutes);
1688+ ToolTipManager.sharedInstance().setInitialDelay(0);
1689+ ToolTipManager.sharedInstance().setReshowDelay(0);
1690+ ToolTipManager.sharedInstance().setEnabled(true);
1691+ }
1692+
1693+ @Override
1694+ public void mouseExited(MouseEvent e) {
1695+ ToolTipManager.sharedInstance().setDismissDelay(defaultDismissTimeout);
1696+ ToolTipManager.sharedInstance().setInitialDelay(defaultInitalDelay);
1697+ ToolTipManager.sharedInstance().setReshowDelay(defaultReshowDelay);
1698+ ToolTipManager.sharedInstance().setEnabled(CreateGui.getApp().isShowingToolTips());
1699+ }
1700+ });
1701+
1702+ TimeDelayField.addKeyListener(new KeyListener() {
1703+ public void keyPressed(KeyEvent e) {
1704+ if (e.getKeyCode() == KeyEvent.VK_ENTER) {
1705+ addTimeDelayToHistory();
1706+ TimeDelayField.getFocusCycleRootAncestor().requestFocus(); // Remove focus
1707+ }
1708+ }
1709+
1710+ public void keyReleased(KeyEvent e) {
1711+ CreateGui.getAnimator().reportBlockingPlaces();
1712+ }
1713+
1714+ public void keyTyped(KeyEvent e) {
1715+
1716+ }
1717+
1718+ });
1719+
1720+ // Disable shortcuts when focused
1721+ TimeDelayField.addFocusListener(new FocusListener() {
1722+ public void focusLost(FocusEvent arg0) {
1723+ CreateGui.getApp().setStepShotcutEnabled(true);
1724+ }
1725+
1726+ public void focusGained(FocusEvent arg0) {
1727+ CreateGui.getApp().setStepShotcutEnabled(false);
1728+ }
1729+ });
1730+
1731+ DecimalFormat df = new DecimalFormat();
1732+ df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
1733+ df.setMinimumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
1734+
1735+ TimeDelayField.setText(df.format(1f));
1736+ TimeDelayField.setColumns(6);
1737+
1738+ timedelayPanel.add(TimeDelayField);
1739+ timedelayPanel.add(okButton);
1740+
1741+ animationToolBar.add(timedelayPanel);
1742+ }
1743
1744 public void updateFiringModeComboBox() {
1745 FiringMode currentFiringMode = CreateGui.getAnimator().getFiringmode();
1746@@ -364,7 +303,7 @@
1747 }
1748
1749 private void addTimeDelayToHistory() {
1750- AnimationHistoryComponent animBox = CreateGui.getAnimationHistory();
1751+ AnimationHistoryComponent animBox = CreateGui.getCurrentTab().getAnimationHistory();
1752 try {
1753
1754 // Hack to allow usage of localised numbes
1755@@ -432,13 +371,10 @@
1756 // number
1757 // localised
1758 // Try parse
1759-
1760 BigDecimal timeDelayToSet = new BigDecimal(parseTime.toString(),
1761 new MathContext(Pipe.AGE_PRECISION));
1762
1763- // BigDecimal timeDelayToSet = new
1764- // BigDecimal(TimeDelayField.getText(), new
1765- // MathContext(Pipe.AGE_PRECISION));
1766+
1767 return timeDelayToSet;
1768 }
1769
1770@@ -453,13 +389,13 @@
1771 }
1772
1773 public void setAnimationButtonsEnabled() {
1774- AnimationHistoryComponent animationHistory = CreateGui.getAnimationHistory();
1775+ AnimationHistoryComponent animationHistory = CreateGui.getCurrentTab().getAnimationHistory();
1776
1777 setEnabledStepforwardAction(animationHistory.isStepForwardAllowed());
1778 setEnabledStepbackwardAction(animationHistory.isStepBackAllowed());
1779
1780- CreateGui.appGui.setEnabledStepForwardAction(animationHistory.isStepForwardAllowed());
1781- CreateGui.appGui.setEnabledStepBackwardAction(animationHistory.isStepBackAllowed());
1782+ CreateGui.getAppGui().setEnabledStepForwardAction(animationHistory.isStepForwardAllowed());
1783+ CreateGui.getAppGui().setEnabledStepBackwardAction(animationHistory.isStepBackAllowed());
1784 }
1785
1786 private void initializeDocumentFilterForDelayInput() {
1787@@ -467,7 +403,5 @@
1788 ((AbstractDocument)doc).setDocumentFilter(new DecimalOnlyDocumentFilter(5));
1789 }
1790
1791- JTextField TimeDelayField = new JTextField();
1792- JComboBox firermodebox = null;
1793- private final String[] FIRINGMODES = { "Random", "Oldest", "Youngest", "Manual" };
1794+
1795 }
1796
1797=== modified file 'src/pipe/gui/AnimationHistoryComponent.java'
1798--- src/pipe/gui/AnimationHistoryComponent.java 2016-11-14 09:58:40 +0000
1799+++ src/pipe/gui/AnimationHistoryComponent.java 2018-07-04 11:38:47 +0000
1800@@ -147,16 +147,16 @@
1801
1802 private void layoutAdjustment() {
1803 // if the trace ends with "deadlock", "delay for ever" or "goto *" makes sure we don't have to scrool to see it
1804- int selectedIndex = CreateGui.getAnimationHistory().getSelectedIndex();
1805- if (selectedIndex == CreateGui.getAnimationHistory().getListModel().getSize()-2) {
1806- CreateGui.getAnimationHistory().setSelectedIndex(selectedIndex+1);
1807- CreateGui.getAnimationHistory().setSelectedIndex(selectedIndex);
1808+ int selectedIndex = CreateGui.getCurrentTab().getAnimationHistory().getSelectedIndex();
1809+ if (selectedIndex == CreateGui.getCurrentTab().getAnimationHistory().getListModel().getSize()-2) {
1810+ CreateGui.getCurrentTab().getAnimationHistory().setSelectedIndex(selectedIndex+1);
1811+ CreateGui.getCurrentTab().getAnimationHistory().setSelectedIndex(selectedIndex);
1812 }
1813 }
1814
1815 private void updateAccordingToDeadlock() {
1816
1817- if(CreateGui.getTab().getSelectedIndex() == -1 || lastShown == TraceType.EG_DELAY_FOREVER){
1818+ if(CreateGui.getApp().getSelectedTabIndex() == -1 || lastShown == TraceType.EG_DELAY_FOREVER){
1819 return;
1820 }
1821 for (Template t : CreateGui.getCurrentTab().activeTemplates()){
1822
1823=== modified file 'src/pipe/gui/AnimationSettings.java'
1824--- src/pipe/gui/AnimationSettings.java 2016-11-14 09:58:40 +0000
1825+++ src/pipe/gui/AnimationSettings.java 2018-07-04 11:38:47 +0000
1826@@ -31,7 +31,7 @@
1827 if(simControl.randomSimulation()){
1828 delayEnabled.randomMode.setSelected(true);
1829 }
1830- CreateGui.getTransitionFireingComponent().updateFireButton();
1831+ CreateGui.getCurrentTab().getTransitionFireingComponent().updateFireButton();
1832 }
1833 });
1834
1835
1836=== modified file 'src/pipe/gui/Animator.java'
1837--- src/pipe/gui/Animator.java 2016-11-14 09:58:40 +0000
1838+++ src/pipe/gui/Animator.java 2018-07-04 11:38:47 +0000
1839@@ -80,20 +80,20 @@
1840 currentAction = -1;
1841 currentMarkingIndex = 0;
1842 tab.network().setMarking(markings.get(currentMarkingIndex));
1843- CreateGui.getAnimationHistory().setSelectedIndex(0);
1844- CreateGui.getAnimationController().setAnimationButtonsEnabled();
1845+ CreateGui.getCurrentTab().getAnimationHistory().setSelectedIndex(0);
1846+ CreateGui.getCurrentTab().getAnimationController().setAnimationButtonsEnabled();
1847 updateFireableTransitions();
1848 }
1849
1850 private void setUntimedTrace(TAPNNetworkTrace trace) {
1851 tab.addAbstractAnimationPane();
1852- AnimationHistoryComponent untimedAnimationHistory = CreateGui.getAbstractAnimationPane();
1853+ AnimationHistoryComponent untimedAnimationHistory = CreateGui.getCurrentTab().getUntimedAnimationHistory();
1854
1855 for(TAPNNetworkTraceStep step : trace){
1856 untimedAnimationHistory.addHistoryItem(step.toString());
1857 }
1858
1859- CreateGui.getAbstractAnimationPane().setSelectedIndex(0);
1860+ CreateGui.getCurrentTab().getUntimedAnimationHistory().setSelectedIndex(0);
1861 setFiringmode("Random");
1862
1863 JOptionPane.showMessageDialog(CreateGui.getApp(),
1864@@ -113,7 +113,7 @@
1865 addMarking(step, step.performStepFrom(currentMarking()));
1866 }
1867 if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock.
1868- CreateGui.getAnimationHistory().setLastShown(getTrace().getTraceType());
1869+ CreateGui.getCurrentTab().getAnimationHistory().setLastShown(getTrace().getTraceType());
1870 }
1871 }
1872
1873@@ -169,7 +169,7 @@
1874 }
1875
1876 public void updateFireableTransitions(){
1877- TransitionFireingComponent transFireComponent = CreateGui.getTransitionFireingComponent();
1878+ TransitionFireingComponent transFireComponent = CreateGui.getCurrentTab().getTransitionFireingComponent();
1879 transFireComponent.startReInit();
1880 isUrgentTransitionEnabled = false;
1881
1882@@ -267,7 +267,7 @@
1883
1884 public void stepForward() {
1885 if(currentAction == actionHistory.size()-1 && trace != null){
1886- int selectedIndex = CreateGui.getAnimationHistory().getSelectedIndex();
1887+ int selectedIndex = CreateGui.getCurrentTab().getAnimationHistory().getSelectedIndex();
1888 int action = currentAction;
1889 int markingIndex = currentMarkingIndex;
1890
1891@@ -278,7 +278,7 @@
1892 addToTimedTrace(getTrace().getLoopSteps());
1893 }
1894
1895- CreateGui.getAnimationHistory().setSelectedIndex(selectedIndex);
1896+ CreateGui.getCurrentTab().getAnimationHistory().setSelectedIndex(selectedIndex);
1897 currentAction = action;
1898 currentMarkingIndex = markingIndex;
1899 }
1900@@ -436,9 +436,9 @@
1901 public void reportBlockingPlaces(){
1902
1903 try{
1904- BigDecimal delay = CreateGui.getAnimationController().getCurrentDelay();
1905+ BigDecimal delay = CreateGui.getCurrentTab().getAnimationController().getCurrentDelay();
1906 if(isUrgentTransitionEnabled && delay.compareTo(new BigDecimal(0))>0){
1907- CreateGui.getAnimationController().getOkButton().setEnabled(false);
1908+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
1909 StringBuilder sb = new StringBuilder();
1910 sb.append("<html>Time delay is disabled due to the<br /> following enabled urgent transitions:<br /><br />");
1911 for( Template temp : CreateGui.getCurrentTab().activeTemplates()){
1912@@ -451,17 +451,17 @@
1913 }
1914 }
1915 sb.append("</html>");
1916- CreateGui.getAnimationController().getOkButton().setToolTipText(sb.toString());
1917+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText(sb.toString());
1918 return;
1919 }
1920 if(delay.compareTo(new BigDecimal(0))<0){
1921- CreateGui.getAnimationController().getOkButton().setEnabled(false);
1922- CreateGui.getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers");
1923+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
1924+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers");
1925 } else {
1926 List<TimedPlace> blockingPlaces = currentMarking().getBlockingPlaces(delay);
1927 if(blockingPlaces.size() == 0){
1928- CreateGui.getAnimationController().getOkButton().setEnabled(true);
1929- CreateGui.getAnimationController().getOkButton().setToolTipText("Press to add the delay");
1930+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(true);
1931+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText("Press to add the delay");
1932 } else {
1933 StringBuilder sb = new StringBuilder();
1934 sb.append("<html>Time delay of " + delay + " time unit(s) is disabled due to <br /> age invariants in the following places:<br /><br />");
1935@@ -470,15 +470,15 @@
1936 }
1937 //JOptionPane.showMessageDialog(null, sb.toString());
1938 sb.append("</html>");
1939- CreateGui.getAnimationController().getOkButton().setEnabled(false);
1940- CreateGui.getAnimationController().getOkButton().setToolTipText(sb.toString());
1941+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
1942+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText(sb.toString());
1943 }
1944 }
1945 } catch (NumberFormatException e) {
1946 // Do nothing, invalud number
1947 } catch (ParseException e) {
1948- CreateGui.getAnimationController().getOkButton().setEnabled(false);
1949- CreateGui.getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number");
1950+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
1951+ CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number");
1952 }
1953 }
1954
1955@@ -514,7 +514,7 @@
1956 removeStoredActions(currentAction + 1);
1957
1958 tab.network().setMarking(marking);
1959- CreateGui.getAnimationHistory().addHistoryItem(action.toString());
1960+ CreateGui.getCurrentTab().getAnimationHistory().addHistoryItem(action.toString());
1961 actionHistory.add(action);
1962 markings.add(marking);
1963 currentAction++;
1964@@ -540,8 +540,8 @@
1965 .println("Illegal firing mode mode: " + t + " not found.");
1966 }
1967
1968- CreateGui.getAnimationController().updateFiringModeComboBox();
1969- CreateGui.getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing");
1970+ CreateGui.getCurrentTab().getAnimationController().updateFiringModeComboBox();
1971+ CreateGui.getCurrentTab().getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing");
1972 }
1973
1974 enum FillListStatus{
1975@@ -644,7 +644,7 @@
1976 if(answer != JOptionPane.OK_OPTION) return false;
1977 }
1978 if(isDisplayingUntimedTrace){
1979- CreateGui.removeAbstractAnimationPane();
1980+ CreateGui.getCurrentTab().removeAbstractAnimationPane();
1981 }
1982 isDisplayingUntimedTrace = false;
1983 trace = null;
1984@@ -661,7 +661,7 @@
1985 answer = removeSetTrace(true);
1986 }
1987 if(answer){
1988- CreateGui.getAnimationHistory().clearStepsForward();
1989+ CreateGui.getCurrentTab().getAnimationHistory().clearStepsForward();
1990 }
1991 return answer;
1992 }
1993
1994=== modified file 'src/pipe/gui/CreateGui.java'
1995--- src/pipe/gui/CreateGui.java 2018-04-21 11:58:41 +0000
1996+++ src/pipe/gui/CreateGui.java 2018-07-04 11:38:47 +0000
1997@@ -1,176 +1,34 @@
1998 package pipe.gui;
1999
2000-import java.awt.Window;
2001-import java.awt.event.ActionEvent;
2002-import java.awt.event.ActionListener;
2003-import java.awt.event.KeyEvent;
2004-import java.io.File;
2005-import java.lang.reflect.Method;
2006 import java.util.ArrayList;
2007-
2008-import javax.swing.JButton;
2009-import javax.swing.JDialog;
2010-import javax.swing.JFrame;
2011-import javax.swing.JOptionPane;
2012-import javax.swing.JTabbedPane;
2013-
2014+import com.sun.jna.Platform;
2015 import net.tapaal.TAPAAL;
2016-import net.tapaal.Preferences;
2017 import pipe.dataLayer.DataLayer;
2018 import pipe.dataLayer.NetType;
2019 import pipe.gui.handler.SpecialMacHandler;
2020 import dk.aau.cs.gui.TabContent;
2021-import dk.aau.cs.gui.components.TransitionFireingComponent;
2022-import dk.aau.cs.verification.UPPAAL.Verifyta;
2023-import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
2024-import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN;
2025-import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification;
2026-
2027-
2028
2029
2030 public class CreateGui {
2031
2032- public static GuiFrame appGui;
2033- private static Animator animator;
2034- private static JTabbedPane appTab;
2035+ private static GuiFrame appGui;
2036 private static ArrayList<TabContent> tabs = new ArrayList<TabContent>();
2037
2038- private static boolean usingGTKFileBrowser = true;
2039-
2040- private static boolean showZeroToInfinityIntervals = true;
2041- private static boolean showTokenAge = true;
2042-
2043- public static String imgPath, userPath; // useful for stuff
2044-
2045- public static Integer MaximalNumberOfTokensAllowed = new Integer(999);
2046-
2047-
2048- public static void checkForUpdate(boolean forcecheck) {
2049- final VersionChecker versionChecker = new VersionChecker();
2050- if (versionChecker.checkForNewVersion(forcecheck)) {
2051- StringBuffer message = new StringBuffer("There is a new version of TAPAAL available at www.tapaal.net.");
2052- message.append("\n\nCurrent version: ");
2053- message.append(TAPAAL.VERSION);
2054- message.append("\nNew version: ");
2055- message.append(versionChecker.getNewVersionNumber());
2056- String changelog = versionChecker.getChangelog();
2057- if (!changelog.equals("")){
2058- message.append('\n');
2059- message.append('\n');
2060- message.append("Changelog:");
2061- message.append('\n');
2062- message.append(changelog);
2063- }
2064- JOptionPane optionPane = new JOptionPane();
2065- optionPane.setMessage(message.toString());
2066- optionPane.setMessageType(JOptionPane.INFORMATION_MESSAGE);
2067- JButton updateButton, laterButton, ignoreButton;
2068- updateButton = new JButton("Update now");
2069- updateButton.setMnemonic(KeyEvent.VK_C);
2070- optionPane.add(updateButton);
2071- laterButton = new JButton("Update later");
2072- laterButton.setMnemonic(KeyEvent.VK_C);
2073- optionPane.add(laterButton);
2074- ignoreButton = new JButton("Ignore this update");
2075- laterButton.setMnemonic(KeyEvent.VK_C);
2076- optionPane.add(ignoreButton);
2077-
2078- optionPane.setOptions(new Object[] {updateButton, laterButton, ignoreButton});
2079-
2080-
2081- final JDialog dialog = optionPane.createDialog(null, "New Version of TAPAAL");
2082- laterButton.addActionListener(new ActionListener() {
2083- public void actionPerformed(ActionEvent e) {
2084- Preferences.getInstance().setLatestVersion(null);
2085- dialog.setVisible(false);
2086- dialog.dispose ();
2087- }
2088- });
2089- updateButton.addActionListener(new ActionListener() {
2090- public void actionPerformed(ActionEvent e) {
2091- Preferences.getInstance().setLatestVersion(null);
2092- dialog.setVisible(false);
2093- dialog.dispose();
2094- pipe.gui.GuiFrame.showInBrowser("http://www.tapaal.net/download");
2095- // appGui.exit();
2096- }
2097- });
2098- ignoreButton.addActionListener(new ActionListener() {
2099- public void actionPerformed(ActionEvent e) {
2100- Preferences.getInstance().setLatestVersion(versionChecker.getNewVersionNumber());
2101- dialog.setVisible(false);
2102- dialog.dispose ();
2103- }
2104- });
2105-
2106- updateButton.requestFocusInWindow();
2107- dialog.getRootPane().setDefaultButton(updateButton);
2108- dialog.setVisible(true);
2109- }
2110- }
2111-
2112+ public static final String imgPath = "resources/Images/";
2113
2114 public static void init() {
2115-
2116- imgPath = "resources/Images/";
2117-
2118- // make the initial dir for browsing be My Documents (win), ~ (*nix),
2119- // etc
2120- userPath = null;
2121-
2122 appGui = new GuiFrame(TAPAAL.getProgramName());
2123-
2124- if (appGui.isMac()){
2125- try {
2126- SpecialMacHandler.postprocess();
2127- } catch (NoClassDefFoundError e) {
2128- //Failed loading special mac handler, ignore and run program without MacOS integration
2129- }
2130+
2131+ if (Platform.isMac()){
2132+ SpecialMacHandler.postprocess();
2133 }
2134-
2135- Grid.enableGrid();
2136-
2137- appTab = new JTabbedPane();
2138-
2139- //TODO
2140- /*
2141- appTab.addChangeListener(new ChangeListener() {
2142- int oldIndex = 0;
2143- @Override
2144- public void stateChanged(ChangeEvent arg0) {
2145- Split model = getTab(oldIndex).getModelRoot();
2146- getCurrentTab().setModelRoot(model);
2147- oldIndex = appTab.getSelectedIndex();
2148- }
2149- });
2150- */
2151-
2152-
2153- animator = new Animator();
2154-
2155- appGui.setTab(); // sets Tab properties
2156-
2157- appGui.getContentPane().add(appTab);
2158-
2159- // appGui.createNewTabFromFile(null);
2160
2161 appGui.setVisible(true);
2162- appGui.activateSelectAction();
2163- Verifyta.trySetup();
2164- VerifyTAPN.trySetup();
2165- VerifyTAPNDiscreteVerification.trySetup();
2166- VerifyPN.trySetup();
2167-
2168- checkForUpdate(false);
2169- }
2170-
2171- public static GuiFrame getApp() { // returns a reference to the application
2172- return appGui;
2173+ appGui.checkForUpdate(false);
2174 }
2175
2176 public static DataLayer getModel() {
2177- return getModel(appTab.getSelectedIndex());
2178+ return getModel(appGui.getSelectedTabIndex());
2179 }
2180
2181 public static DataLayer getModel(int index) {
2182@@ -183,7 +41,7 @@
2183 }
2184
2185 public static DrawingSurfaceImpl getDrawingSurface() {
2186- return getDrawingSurface(appTab.getSelectedIndex());
2187+ return getDrawingSurface(appGui.getSelectedTabIndex());
2188 }
2189
2190 public static DrawingSurfaceImpl getDrawingSurface(int index) {
2191@@ -193,175 +51,60 @@
2192 }
2193
2194 TabContent tab = (tabs.get(index));
2195- while (tab.drawingSurface() == null) {
2196-
2197- try {
2198- tab.setDrawingSurface(new DrawingSurfaceImpl(tab.getModel()));
2199- } catch (Exception e) {
2200- e.printStackTrace();
2201- }
2202- }
2203+
2204+ //XXX: 2018-04-26//kyrke The following code should never be called, a TAB always has a driwingSurface,
2205+ // if not seems wired to just create it.
2206+ // Code left in place for history, in case we someday experience problems with this.
2207+ // If no problems have been observed for some time, please remove the code and comment.
2208+// while (tab.drawingSurface() == null) {
2209+//
2210+// try {
2211+// tab.setDrawingSurface(new DrawingSurfaceImpl(tab.getModel(),
2212+// tab));
2213+// } catch (Exception e) {
2214+// e.printStackTrace();
2215+// }
2216+// }
2217+
2218 return tab.drawingSurface();
2219 }
2220
2221- public static DrawingSurfaceImpl getView() {
2222- return getDrawingSurface(appTab.getSelectedIndex());
2223- }
2224-
2225- public static File getFile() {
2226- return getFile(appTab.getSelectedIndex());
2227- }
2228-
2229- public static void setFile(File modelfile, int fileNo) {
2230- if (fileNo >= tabs.size()) {
2231- return;
2232- }
2233-
2234- TabContent tab = (tabs.get(fileNo));
2235- tab.setFile(modelfile);
2236-
2237- }
2238
2239 public static int getFreeSpace(NetType netType) {
2240 tabs.add(new TabContent(netType));
2241 return tabs.size() - 1;
2242 }
2243
2244+ public static void addTab (TabContent tab ) {
2245+ tabs.add(tab);
2246+ }
2247+
2248 public static void removeTab(int index) {
2249 tabs.remove(index);
2250 }
2251
2252- public static JTabbedPane getTab() {
2253- return appTab;
2254- }
2255-
2256 public static TabContent getTab(int index) {
2257 return tabs.get(index);
2258 }
2259
2260 public static TabContent getCurrentTab() {
2261- return tabs.get(appTab.getSelectedIndex());
2262- }
2263-
2264- public static Animator getAnimator() {
2265- return animator;
2266+ return getTab(appGui.getSelectedTabIndex());
2267 }
2268
2269 /**
2270- * returns the current dataLayer object - used to get a reference to pass to
2271- * the modules
2272+ * @deprecated Use method getAnimator in GuiFrame
2273+ * @return
2274 */
2275- public static DataLayer currentPNMLData() {
2276- if (appTab.getSelectedIndex() < 0) {
2277- return null;
2278- }
2279-
2280- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2281- return tab.getModel();
2282- }
2283-
2284- /** Creates a new animationHistory text area, and returns a reference to it */
2285- public static void switchToAnimationComponents() {
2286- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2287- tab.switchToAnimationComponents(true);
2288- }
2289-
2290- public static void switchToEditorComponents() {
2291- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2292- tab.switchToEditorComponents();
2293- }
2294-
2295- public static AnimationHistoryComponent getAbstractAnimationPane() {
2296- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2297- return tab.getUntimedAnimationHistory();
2298-
2299- }
2300-
2301- public static void addAbstractAnimationPane() {
2302- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2303- tab.addAbstractAnimationPane();
2304- }
2305-
2306- public static AnimationController getAnimationController() {
2307- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2308- return tab.getAnimationController();
2309-
2310- }
2311-
2312-
2313- public static TransitionFireingComponent getTransitionFireingComponent() {
2314- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2315- return tab.getTransitionFireingComponent();
2316-
2317- }
2318-
2319- public static void removeAbstractAnimationPane() {
2320- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2321- tab.removeAbstractAnimationPane();
2322- }
2323-
2324- // public static void addAnimationController() {
2325- // TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2326- // //tab.addAnimationController();
2327- // }
2328-
2329- // public static void removeAnimationHistory() {
2330- // TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2331- // tab.removeAnimationHistory();
2332- // }
2333- //
2334- // public static void removeAnimationController() {
2335- // TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2336- // tab.removeAnimationController();
2337- // }
2338-
2339- public static AnimationHistoryComponent getAnimationHistory() {
2340- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2341- return tab.getAnimationHistory();
2342- }
2343-
2344- public static void updateConstantsList() {
2345- TabContent tab = (tabs.get(appTab.getSelectedIndex()));
2346- tab.updateConstantsList();
2347- }
2348-
2349- public static void undoGetFreeSpace() {
2350- tabs.remove(tabs.size() - 1);
2351- }
2352-
2353- public static File getFile(int index) {
2354- TabContent tab = tabs.get(index);
2355- return tab.getFile();
2356- }
2357-
2358- public static void setUsingGTKFileBrowser(boolean useGTKFileBrowser) {
2359- usingGTKFileBrowser = useGTKFileBrowser;
2360- }
2361-
2362- public static boolean usingGTKFileBrowser() {
2363- return usingGTKFileBrowser;
2364- }
2365-
2366- public static void toggleShowZeroToInfinityIntervals() {
2367- showZeroToInfinityIntervals = !showZeroToInfinityIntervals;
2368- }
2369-
2370- public static boolean showZeroToInfinityIntervals() {
2371- return showZeroToInfinityIntervals;
2372- }
2373-
2374- public static boolean showTokenAge(){
2375- return showTokenAge;
2376- }
2377-
2378- public static void toggleShowTokenAge(){
2379- showTokenAge = !showTokenAge;
2380- }
2381-
2382- public static void verifyQuery() {
2383- TabContent tab = getCurrentTab();
2384- if (tab.isQueryPossible()) {
2385- getCurrentTab().verifySelectedQuery();
2386- }
2387+ @Deprecated
2388+ public static Animator getAnimator() {
2389+ return appGui.getAnimator();
2390+ }
2391+
2392+ //XXX Two Methodes to access same data (created after auto encapsulate)
2393+ public static GuiFrame getApp() { // returns a reference to the application
2394+ return getAppGui();
2395+ }
2396+ public static GuiFrame getAppGui() {
2397+ return appGui;
2398 }
2399 }
2400
2401=== modified file 'src/pipe/gui/DelayEnabledTransitionControl.java'
2402--- src/pipe/gui/DelayEnabledTransitionControl.java 2016-11-14 09:58:40 +0000
2403+++ src/pipe/gui/DelayEnabledTransitionControl.java 2018-07-04 11:38:47 +0000
2404@@ -33,10 +33,10 @@
2405 private static BigDecimal defaultGranularity = new BigDecimal("0.1");
2406 private static boolean defaultIsRandomTrasition;
2407
2408- JLabel precitionLabel;
2409- JSlider delayEnabledPrecision;
2410- JLabel delayModeLabel;
2411- JComboBox delayMode;
2412+ private JLabel precitionLabel;
2413+ private JSlider delayEnabledPrecision;
2414+ private JLabel delayModeLabel;
2415+ private JComboBox delayMode;
2416 JCheckBox randomMode;
2417
2418 private DelayEnabledTransitionControl() {
2419@@ -45,12 +45,12 @@
2420 //0 corresponds to 0.00001, 5 corresponds to 1 ( thus x corresponds to 1/(10^(5−x)) )
2421 delayEnabledPrecision = new JSlider(JSlider.HORIZONTAL, 0, 5, 4);
2422 Hashtable<Integer, JLabel> labelTable = new Hashtable<Integer, JLabel>();
2423- labelTable.put(new Integer(0), new JLabel("0.00001"));
2424- labelTable.put(new Integer(1), new JLabel("0.0001"));
2425- labelTable.put(new Integer(2), new JLabel("0.001"));
2426- labelTable.put(new Integer(3), new JLabel("0.01"));
2427- labelTable.put(new Integer(4), new JLabel("0.1"));
2428- labelTable.put(new Integer(5), new JLabel("1"));
2429+ labelTable.put(0, new JLabel("0.00001"));
2430+ labelTable.put(1, new JLabel("0.0001"));
2431+ labelTable.put(2, new JLabel("0.001"));
2432+ labelTable.put(3, new JLabel("0.01"));
2433+ labelTable.put(4, new JLabel("0.1"));
2434+ labelTable.put(5, new JLabel("1"));
2435
2436 delayEnabledPrecision.setLabelTable(labelTable);
2437 delayEnabledPrecision.setSnapToTicks(true);
2438
2439=== modified file 'src/pipe/gui/DrawingSurfaceImpl.java'
2440--- src/pipe/gui/DrawingSurfaceImpl.java 2018-04-21 11:58:41 +0000
2441+++ src/pipe/gui/DrawingSurfaceImpl.java 2018-07-04 11:38:47 +0000
2442@@ -32,7 +32,6 @@
2443 import pipe.gui.undo.AddTimedPlaceCommand;
2444 import pipe.gui.undo.AddTimedTransitionCommand;
2445 import pipe.gui.undo.UndoManager;
2446-import dk.aau.cs.gui.DrawingSurface;
2447 import dk.aau.cs.gui.NameGenerator;
2448 import dk.aau.cs.gui.TabContent;
2449 import dk.aau.cs.model.tapn.TimedArcPetriNet;
2450@@ -41,15 +40,14 @@
2451 * The petrinet is drawn onto this frame.
2452 */
2453 public class DrawingSurfaceImpl extends JLayeredPane implements Observer,
2454-Printable, DrawingSurface {
2455+Printable {
2456 private static final long serialVersionUID = 4434596266503933386L;
2457 private boolean netChanged = false;
2458 private boolean animationmode = false;
2459
2460 public Arc createArc; // no longer static
2461- public PlaceTransitionObject createPTO;
2462
2463- protected static final int DRAWING_SURFACE_GROW = 100;
2464+ private static final int DRAWING_SURFACE_GROW = 100;
2465
2466 private AnimationHandler animationHandler = new AnimationHandler();
2467
2468@@ -59,9 +57,6 @@
2469 private GuiFrame app = CreateGui.getApp();
2470 private Zoomer zoomControl;
2471
2472- // flag used in fast mode to know if a new PetriNetObject has been created
2473- public boolean newPNO = false;
2474-
2475 // flag used in paintComponents() to know if a call to zoom() has been done
2476 private boolean doSetViewPosition = true;
2477
2478@@ -87,7 +82,7 @@
2479 mouseHandler = new MouseHandler(this, dataLayer);
2480 addMouseListener(mouseHandler);
2481 addMouseMotionListener(mouseHandler);
2482- //addMouseWheelListener(mouseHandler);
2483+ addMouseWheelListener(mouseHandler);
2484
2485 selection = new SelectionManager(this);
2486 undoManager = new UndoManager(this, guiModel, app);
2487@@ -129,9 +124,9 @@
2488 add(pnObject);
2489 }
2490
2491- if(CreateGui.getApp().getMode() == ElementType.SELECT)
2492+ if(CreateGui.getApp().getMode() == ElementType.SELECT) {
2493 this.selection.enableSelection();
2494-
2495+ }
2496
2497 }
2498
2499@@ -229,7 +224,7 @@
2500
2501 public void update(Observable o, Object diffObj) {
2502 if ((diffObj instanceof PetriNetObject) && (diffObj != null)) {
2503- if (CreateGui.appGui.getMode() == ElementType.CREATING) {
2504+ if (CreateGui.getAppGui().getMode() == ElementType.CREATING) {
2505
2506 addNewPetriNetObject((PetriNetObject) diffObj);
2507 }
2508@@ -321,16 +316,6 @@
2509 }
2510 }
2511
2512- public void setCursorType(String type) {
2513- if (type.equals("arrow")) {
2514- setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
2515- } else if (type.equals("crosshair")) {
2516- setCursor(Cursor.getPredefinedCursor(Cursor.CROSSHAIR_CURSOR));
2517- } else if (type.equals("move")) {
2518- setCursor(Cursor.getPredefinedCursor(Cursor.MOVE_CURSOR));
2519- }
2520- }
2521-
2522 public SelectionManager getSelectionObject() {
2523 return selection;
2524 }
2525@@ -355,7 +340,7 @@
2526 }
2527 }
2528
2529- public void calculateNewBoundsForScrollPane(Rectangle rect) {
2530+ private void calculateNewBoundsForScrollPane(Rectangle rect) {
2531 boolean changed = false;
2532 Dimension current = getPreferredSize();
2533
2534@@ -457,6 +442,13 @@
2535 return (new java.awt.Point((int) midpointX, (int) midpointY));
2536 }
2537
2538+ void zoomToMidPoint() {
2539+
2540+ Point midpoint = midpoint(zoomControl.getPercent());
2541+ zoomTo(midpoint);
2542+
2543+ }
2544+
2545 public void zoomIn() {
2546 int zoom = zoomControl.getPercent();
2547 if (zoomControl.zoomIn()) {
2548@@ -612,7 +604,7 @@
2549 getUndoManager().addNewEdit(
2550 new AddPetriNetObjectEdit(pto, view, guiModel));
2551 if (e.isControlDown()) {
2552- app.setFastMode(ElementType.FAST_TRANSITION);
2553+ app.setMode(ElementType.FAST_TRANSITION);
2554 pnObject.dispatchEvent(e);
2555 }
2556 break;
2557@@ -629,7 +621,7 @@
2558 app.setMode(ElementType.TAPNARC);
2559 getPlaceTransitionObjectHandlerOf(pto2).mousePressed(e);
2560 getPlaceTransitionObjectHandlerOf(pto2).mouseReleased(e);
2561- app.setFastMode(ElementType.FAST_TRANSITION);
2562+ app.setMode(ElementType.FAST_TRANSITION);
2563 // enter fast mode
2564 pnObject.dispatchEvent(e);
2565 }
2566@@ -637,12 +629,12 @@
2567
2568 case IMMTRANS:
2569 case TIMEDTRANS:
2570- boolean timed = (mode == ElementType.TIMEDTRANS ? true : false);
2571+ boolean timed = (mode == ElementType.TIMEDTRANS);
2572 pto = newTransition(e.getPoint(), timed);
2573 getUndoManager().addNewEdit(
2574 new AddPetriNetObjectEdit(pto, view, guiModel));
2575 if (e.isControlDown()) {
2576- app.setFastMode(ElementType.FAST_PLACE);
2577+ app.setMode(ElementType.FAST_PLACE);
2578 pnObject.dispatchEvent(e);
2579 }
2580 break;
2581@@ -659,7 +651,7 @@
2582 getPlaceTransitionObjectHandlerOf(pto).mousePressed(e);
2583 getPlaceTransitionObjectHandlerOf(pto).mouseReleased(e);
2584 // enter fast mode
2585- app.setFastMode(ElementType.FAST_PLACE);
2586+ app.setMode(ElementType.FAST_PLACE);
2587 pnObject.dispatchEvent(e);
2588 }
2589 break;
2590@@ -714,7 +706,7 @@
2591 getPlaceTransitionObjectHandlerOf(pto).mousePressed(e);
2592 getPlaceTransitionObjectHandlerOf(pto).mouseReleased(e);
2593 // enter fast mode
2594- app.setFastMode(ElementType.FAST_PLACE);
2595+ app.setMode(ElementType.FAST_PLACE);
2596 } else{
2597 app.endFastMode();
2598 }
2599@@ -733,7 +725,7 @@
2600 getPlaceTransitionObjectHandlerOf(pto3).mousePressed(e);
2601 getPlaceTransitionObjectHandlerOf(pto3).mouseReleased(e);
2602 // enter fast mode
2603- app.setFastMode(ElementType.FAST_TRANSITION);
2604+ app.setMode(ElementType.FAST_TRANSITION);
2605 } else{
2606 app.endFastMode();
2607 }
2608@@ -789,14 +781,15 @@
2609
2610 @Override
2611 public void mouseWheelMoved(MouseWheelEvent e) {
2612- if (!e.isControlDown()) {
2613- return;
2614- } else {
2615+ if (e.isControlDown()) {
2616 if (e.getWheelRotation() > 0) {
2617 view.zoomIn();
2618 } else {
2619 view.zoomOut();
2620 }
2621+ } else {
2622+ //Dispatch Event to scroll pane to allow scrolling up/down. -- kyrke
2623+ getParent().dispatchEvent(e);
2624 }
2625 }
2626 }
2627
2628=== modified file 'src/pipe/gui/Export.java'
2629--- src/pipe/gui/Export.java 2018-05-11 16:23:59 +0000
2630+++ src/pipe/gui/Export.java 2018-07-04 11:38:47 +0000
2631@@ -29,7 +29,6 @@
2632 import javax.print.SimpleDoc;
2633 import javax.print.StreamPrintServiceFactory;
2634 import javax.print.attribute.HashPrintRequestAttributeSet;
2635-import javax.swing.JComponent;
2636 import javax.swing.JOptionPane;
2637 import javax.xml.parsers.ParserConfigurationException;
2638 import javax.xml.transform.TransformerConfigurationException;
2639@@ -52,7 +51,7 @@
2640 import pipe.dataLayer.TAPNQuery;
2641 import pipe.gui.GuiFrame.GUIMode;
2642 import pipe.gui.graphicElements.PetriNetObject;
2643-import pipe.gui.widgets.FileBrowser;
2644+import pipe.gui.widgets.filebrowser.FileBrowser;
2645
2646 /**
2647 * Class for exporting things to other formats, as well as printing.
2648@@ -182,8 +181,8 @@
2649 }
2650
2651 String filename = null;
2652- if (CreateGui.getFile() != null) {
2653- filename = CreateGui.getFile().getAbsolutePath();
2654+ if (CreateGui.getCurrentTab().getFile() != null) {
2655+ filename = CreateGui.getCurrentTab().getFile().getAbsolutePath();
2656 // change file extension
2657 int dotpos = filename.lastIndexOf('.');
2658 if (dotpos > filename.lastIndexOf(System.getProperty("file.separator"))) {
2659@@ -217,13 +216,13 @@
2660 try {
2661 switch (format) {
2662 case PNG:
2663- filename = new FileBrowser("PNG image", "png", filename).saveFile();
2664+ filename = FileBrowser.constructor("PNG image", "png", filename).saveFile();
2665 if (filename != null) {
2666 toPNG(g, filename);
2667 }
2668 break;
2669 case POSTSCRIPT:
2670- filename = new FileBrowser("PostScript file", "ps", filename)
2671+ filename = FileBrowser.constructor("PostScript file", "ps", filename)
2672 .saveFile();
2673 if (filename != null) {
2674 toPostScript(g, filename);
2675@@ -249,21 +248,21 @@
2676 if (figureOptions == possibilities[1])
2677 tikZOption = TikZExporter.TikZOutputOption.FULL_LATEX;
2678
2679- filename = new FileBrowser("TikZ figure", "tex", filename).saveFile();
2680+ filename = FileBrowser.constructor("TikZ figure", "tex", filename).saveFile();
2681 if (filename != null) {
2682 TikZExporter output = new TikZExporter(model, filename, tikZOption);
2683 output.ExportToTikZ();
2684 }
2685 break;
2686 case PNML:
2687- filename = new FileBrowser("PNML file", "pnml", filename)
2688+ filename = FileBrowser.constructor("PNML file", "pnml", filename)
2689 .saveFile();
2690 if (filename != null) {
2691 toPnml(g, filename);
2692 }
2693 break;
2694 case QUERY:
2695- filename = new FileBrowser("Query XML file", "xml", filename).saveFile(CreateGui.appGui.getCurrentTabName().replaceAll(".xml", "-queries"));
2696+ filename = FileBrowser.constructor("Query XML file", "xml", filename).saveFile(CreateGui.getAppGui().getCurrentTabName().replaceAll(".xml", "-queries"));
2697 if (filename != null) {
2698 toQueryXML(filename);
2699 }
2700
2701=== modified file 'src/pipe/gui/ExportBatchDialog.java'
2702--- src/pipe/gui/ExportBatchDialog.java 2018-05-07 14:49:44 +0000
2703+++ src/pipe/gui/ExportBatchDialog.java 2018-07-04 11:38:47 +0000
2704@@ -50,17 +50,14 @@
2705 import javax.xml.transform.TransformerException;
2706 import org.w3c.dom.DOMException;
2707 import dk.aau.cs.gui.FileNameCellRenderer;
2708-import dk.aau.cs.gui.components.BatchProcessingResultsTableModel;
2709 import dk.aau.cs.gui.components.ExportBatchResultTableModel;
2710 import dk.aau.cs.io.LoadedModel;
2711 import dk.aau.cs.io.ModelLoader;
2712 import dk.aau.cs.io.PNMLWriter;
2713 import dk.aau.cs.model.tapn.TimedArcPetriNet;
2714 import dk.aau.cs.util.StringComparator;
2715-import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationResult;
2716 import pipe.dataLayer.DataLayer;
2717-import pipe.dataLayer.TAPNQuery;
2718-import pipe.gui.widgets.FileBrowser;
2719+import pipe.gui.widgets.filebrowser.FileBrowser;
2720
2721 public class ExportBatchDialog extends JDialog {
2722
2723@@ -416,7 +413,7 @@
2724 }
2725
2726 private void addFiles() {
2727- FileBrowser browser = new FileBrowser("Timed-Arc Petri Nets",".xml", lastSelectPath);
2728+ FileBrowser browser = FileBrowser.constructor("Timed-Arc Petri Nets", "xml", lastSelectPath);
2729
2730 File[] filesArray = browser.openFiles();
2731 if (filesArray.length>0) {
2732@@ -466,7 +463,7 @@
2733 }
2734
2735 private void selectDestinationPath() {
2736- String chosenFile = new FileBrowser("Select an export folder", ".", lastExportPath).saveFile("Export");
2737+ String chosenFile = FileBrowser.constructor("Select an export folder", ".", lastExportPath).saveFile("Export");
2738 if(chosenFile != null) {
2739 destinationFile = new File(chosenFile);
2740 lastExportPath = chosenFile;
2741
2742=== removed file 'src/pipe/gui/ExtensionFilter.java'
2743--- src/pipe/gui/ExtensionFilter.java 2011-02-03 19:03:15 +0000
2744+++ src/pipe/gui/ExtensionFilter.java 1970-01-01 00:00:00 +0000
2745@@ -1,32 +0,0 @@
2746-/*
2747- * Created on 16-Feb-2004
2748- */
2749-package pipe.gui;
2750-
2751-import java.io.File;
2752-
2753-import javax.swing.filechooser.FileFilter;
2754-
2755-public class ExtensionFilter extends FileFilter {
2756-
2757- protected String myExtensionString; // The extension we will accept
2758- protected String myExtensionDesc; // A description of its meaning
2759-
2760- public ExtensionFilter(String ext, String desc) {
2761- myExtensionString = ext.toLowerCase();
2762- myExtensionDesc = desc;
2763- }
2764-
2765- @Override
2766- public boolean accept(File f) {
2767- return f.isDirectory()
2768- || f.getName().toLowerCase().endsWith(myExtensionString);
2769- } // Don't want directories, especially ones which end with the desired
2770- // extension!
2771-
2772- @Override
2773- public String getDescription() {
2774- return myExtensionDesc;
2775- }
2776-
2777-}
2778
2779=== modified file 'src/pipe/gui/FileFinder.java'
2780--- src/pipe/gui/FileFinder.java 2013-03-22 19:37:07 +0000
2781+++ src/pipe/gui/FileFinder.java 2018-07-04 11:38:47 +0000
2782@@ -1,7 +1,16 @@
2783 package pipe.gui;
2784
2785+import pipe.gui.widgets.filebrowser.FileBrowser;
2786+
2787 import java.io.File;
2788
2789-public interface FileFinder {
2790- File ShowFileBrowserDialog(String description, String extension, String path);
2791+
2792+public class FileFinder {
2793+
2794+ public File ShowFileBrowserDialog(String description, String extension, String path) {
2795+ if (path==null || path=="") { path= System.getProperty("user.home"); }
2796+ FileBrowser fileBrowser = FileBrowser.constructor(description, extension, path);
2797+ return fileBrowser.openFile();
2798+ }
2799+
2800 }
2801
2802=== removed file 'src/pipe/gui/FileFinderImpl.java'
2803--- src/pipe/gui/FileFinderImpl.java 2013-03-22 19:37:07 +0000
2804+++ src/pipe/gui/FileFinderImpl.java 1970-01-01 00:00:00 +0000
2805@@ -1,15 +0,0 @@
2806-package pipe.gui;
2807-
2808-import java.io.File;
2809-
2810-import pipe.gui.widgets.FileBrowser;
2811-
2812-public class FileFinderImpl implements FileFinder {
2813-
2814- public File ShowFileBrowserDialog(String description, String extension, String path) {
2815- if (path==null || path=="") { path= System.getProperty("user.home"); }
2816- FileBrowser fileBrowser = new FileBrowser(description, extension, path);
2817- return fileBrowser.openFile();
2818- }
2819-
2820-}
2821
2822=== modified file 'src/pipe/gui/GuiFrame.java'
2823--- src/pipe/gui/GuiFrame.java 2018-05-11 13:19:26 +0000
2824+++ src/pipe/gui/GuiFrame.java 2018-07-04 11:38:47 +0000
2825@@ -17,38 +17,14 @@
2826 import java.util.jar.JarEntry;
2827 import java.util.jar.JarFile;
2828 import javax.imageio.ImageIO;
2829-import javax.swing.Action;
2830-import javax.swing.BoxLayout;
2831-import javax.swing.DefaultListModel;
2832-import javax.swing.ImageIcon;
2833-import javax.swing.JCheckBox;
2834-import javax.swing.JCheckBoxMenuItem;
2835-import javax.swing.JComboBox;
2836-import javax.swing.JComponent;
2837-import javax.swing.JDialog;
2838-import javax.swing.JFrame;
2839-import javax.swing.JList;
2840-import javax.swing.JMenu;
2841-import javax.swing.JMenuBar;
2842-import javax.swing.JMenuItem;
2843-import javax.swing.JOptionPane;
2844-import javax.swing.JPanel;
2845-import javax.swing.JTabbedPane;
2846-import javax.swing.JToggleButton;
2847-import javax.swing.JToolBar;
2848-import javax.swing.JViewport;
2849-import javax.swing.KeyStroke;
2850-import javax.swing.ToolTipManager;
2851-import javax.swing.UIDefaults;
2852-import javax.swing.UIManager;
2853-import javax.swing.UIManager.LookAndFeelInfo;
2854-import javax.swing.UnsupportedLookAndFeelException;
2855+import javax.swing.*;
2856 import javax.swing.event.ChangeEvent;
2857 import javax.swing.event.ChangeListener;
2858
2859 import com.apple.eawt.Application;
2860 import dk.aau.cs.gui.TabTransformer;
2861 import dk.aau.cs.model.tapn.*;
2862+import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
2863 import net.tapaal.Preferences;
2864 import com.sun.jna.Platform;
2865
2866@@ -71,10 +47,9 @@
2867 import pipe.gui.undo.ChangeSpacingEdit;
2868 import pipe.gui.widgets.EngineDialogPanel;
2869 import pipe.gui.widgets.EscapableDialog;
2870-import pipe.gui.widgets.FileBrowser;
2871+import pipe.gui.widgets.filebrowser.FileBrowser;
2872 import pipe.gui.widgets.NewTAPNPanel;
2873 import pipe.gui.widgets.QueryDialog;
2874-import pipe.gui.widgets.QueryPane;
2875 import pipe.gui.widgets.WorkflowDialog;
2876 import dk.aau.cs.debug.Logger;
2877 import dk.aau.cs.gui.BatchProcessingDialog;
2878@@ -101,39 +76,70 @@
2879
2880 private static final long serialVersionUID = 7509589834941127217L;
2881 // for zoom combobox and dropdown
2882- private final String[] zoomExamples = { "40%", "60%", "80%", "100%",
2883- "120%", "140%", "160%", "180%", "200%", "300%" };
2884- private String frameTitle; // Frame title
2885- private GuiFrame appGui;
2886+ private final int[] zoomExamples = { 40, 60, 80, 100,
2887+ 120, 140, 160, 180, 200, 300 };
2888+
2889+ private String frameTitle;
2890 private DrawingSurfaceImpl appView;
2891- private Pipe.ElementType mode, prev_mode, old_mode; // *** mode WAS STATIC ***
2892+
2893+ public Animator getAnimator() {
2894+ return animator;
2895+ }
2896+
2897+ private Animator animator;
2898+ private Pipe.ElementType mode, prev_mode;
2899+ private GUIMode guiMode = GUIMode.noNet;
2900+
2901 private int newNameCounter = 1;
2902+
2903 private JTabbedPane appTab;
2904+
2905 private StatusBar statusBar;
2906 private JMenuBar menuBar;
2907 private JToolBar drawingToolBar;
2908- private JComboBox zoomComboBox;
2909-
2910- private FileAction createAction, openAction, closeAction, saveAction,
2911- saveAsAction, exitAction, printAction, importPNMLAction, importSUMOAction,
2912- importXMLAction, exportPNGAction, exportPSAction, exportToTikZAction,
2913- exportToPNMLAction, exportToXMLAction, exportTraceAction, importTraceAction,
2914- exportBatchAction;
2915-
2916- private VerificationAction runUppaalVerification;
2917-
2918- private EditAction /* copyAction, cutAction, pasteAction, */undoAction, redoAction;
2919- private GridAction toggleGrid;
2920- private ToolAction netStatisticsAction, batchProcessingAction, engineSelectionAction, verifyAction, workflowDialogAction, stripTimeDialogAction;
2921- private ZoomAction zoomOutAction, zoomInAction;
2922- private SpacingAction incSpacingAction, decSpacingAction;
2923- private DeleteAction deleteAction;
2924- private SelectAllAction selectAllAction;
2925- private TypeAction annotationAction, arcAction, inhibarcAction,
2926- placeAction, transAction, timedtransAction, tokenAction,
2927- selectAction, deleteTokenAction, timedPlaceAction;
2928- private ViewAction showTokenAgeAction, showComponentsAction, showQueriesAction, showConstantsAction,showZeroToInfinityIntervalsAction,showEnabledTransitionsAction, showDelayEnabledTransitionsAction,showToolTipsAction,showAdvancedWorkspaceAction,showSimpleWorkspaceAction,saveWorkSpaceAction;
2929- private HelpAction showAboutAction, showHomepage, showAskQuestionAction, showReportBugAction, showFAQAction, checkUpdate;
2930+ private JComboBox<String> zoomComboBox;
2931+
2932+ private GuiAction createAction;
2933+ private GuiAction openAction;
2934+ private GuiAction closeAction;
2935+ private GuiAction saveAction;
2936+ private GuiAction saveAsAction;
2937+ private GuiAction exitAction;
2938+ private GuiAction printAction;
2939+ private GuiAction importPNMLAction;
2940+ private GuiAction importSUMOAction;
2941+ private GuiAction importXMLAction;
2942+ private GuiAction exportPNGAction;
2943+ private GuiAction exportPSAction;
2944+ private GuiAction exportToTikZAction;
2945+ private GuiAction exportToPNMLAction;
2946+ private GuiAction exportToXMLAction;
2947+ private GuiAction exportTraceAction;
2948+ private GuiAction importTraceAction;
2949+ private GuiAction exportBatchAction;
2950+
2951+ private GuiAction /* copyAction, cutAction, pasteAction, */undoAction, redoAction;
2952+ private GuiAction toggleGrid;
2953+ private GuiAction netStatisticsAction;
2954+ private GuiAction batchProcessingAction;
2955+ private GuiAction engineSelectionAction;
2956+ private GuiAction verifyAction;
2957+ private GuiAction workflowDialogAction;
2958+ private GuiAction stripTimeDialogAction;
2959+ private GuiAction zoomOutAction;
2960+ private GuiAction zoomInAction;
2961+
2962+ private GuiAction incSpacingAction;
2963+ private GuiAction decSpacingAction;
2964+ public GuiAction deleteAction;
2965+
2966+ private TypeAction annotationAction;
2967+ private TypeAction inhibarcAction;
2968+ private TypeAction transAction;
2969+ private TypeAction tokenAction;
2970+ private TypeAction selectAction;
2971+ private TypeAction deleteTokenAction;
2972+ private TypeAction timedPlaceAction;
2973
2974 private JMenuItem statistics;
2975 private JMenuItem verification;
2976@@ -141,25 +147,40 @@
2977 private TypeAction timedArcAction;
2978 private TypeAction transportArcAction;
2979
2980-
2981- public AnimateAction startAction, stepforwardAction, stepbackwardAction,
2982- randomAction, randomAnimateAction, timeAction, delayFireAction, prevcomponentAction, nextcomponentAction;
2983-
2984- public boolean dragging = false;
2985-
2986- private boolean editionAllowed = true;
2987+ private GuiAction showTokenAgeAction;
2988+ private GuiAction showComponentsAction;
2989+ private GuiAction showQueriesAction;
2990+ private GuiAction showConstantsAction;
2991+ private GuiAction showZeroToInfinityIntervalsAction;
2992+ private GuiAction showEnabledTransitionsAction;
2993+ private GuiAction showDelayEnabledTransitionsAction;
2994+ private GuiAction showToolTipsAction;
2995+ private GuiAction showAdvancedWorkspaceAction;
2996+ private GuiAction showSimpleWorkspaceAction;
2997+ private GuiAction saveWorkSpaceAction;
2998+ private GuiAction showAboutAction;
2999+ private GuiAction showHomepage;
3000+ private GuiAction showAskQuestionAction;
3001+ private GuiAction showReportBugAction;
3002+ private GuiAction showFAQAction;
3003+ private GuiAction checkUpdate;
3004+
3005+
3006+ private GuiAction selectAllAction;
3007+
3008+ public GuiAction startAction;
3009+ public GuiAction stepforwardAction;
3010+ public GuiAction stepbackwardAction;
3011+ private GuiAction timeAction;
3012+ private GuiAction delayFireAction;
3013+ private GuiAction prevcomponentAction;
3014+ private GuiAction nextcomponentAction;
3015
3016 public enum GUIMode {
3017 draw, animation, noNet
3018 }
3019
3020 private JCheckBoxMenuItem showZeroToInfinityIntervalsCheckBox;
3021- private JCheckBoxMenuItem showComponentsCheckBox;
3022- private JCheckBoxMenuItem showQueriesCheckBox;
3023- private JCheckBoxMenuItem showEnabledTransitionsCheckBox;
3024- private JCheckBoxMenuItem showDelayEnabledTransitionsCheckBox;
3025- private JCheckBoxMenuItem showConstantsCheckBox;
3026- private JCheckBoxMenuItem showToolTipsCheckBox;
3027 private JCheckBoxMenuItem showTokenAgeCheckBox;
3028
3029 private boolean showComponents = true;
3030@@ -168,49 +189,101 @@
3031 private boolean showEnabledTransitions = true;
3032 private boolean showDelayEnabledTransitions = true;
3033 private boolean showToolTips = true;
3034-
3035- private GUIMode guiMode = GUIMode.noNet;
3036+ private boolean showZeroToInfinityIntervals = true;
3037+ private boolean showTokenAge = true;
3038+
3039+
3040 private JMenu importMenu, exportMenu, zoomMenu;
3041
3042-
3043- public boolean isMac(){
3044- return Platform.isMac();
3045- }
3046-
3047- public int getJRE(){
3048- String version = System.getProperty("java.version");
3049- String[] versionSplit = version.split("\\.");
3050-
3051- try {
3052- if (Integer.parseInt(versionSplit[0]) >= 9) {
3053- //Version format (9.X.Y)
3054- return Integer.parseInt(versionSplit[0]);
3055- } else {
3056- //Before java 9 version in format (1.X.Y)
3057- return Integer.parseInt(versionSplit[1]);
3058- }
3059- } catch (NumberFormatException e) {
3060- Logger.log("Error parsing java version, failing silent (0): " + e.getMessage());
3061- return 0; // Unknown version
3062- }
3063- }
3064-
3065 public GuiFrame(String title) {
3066 // HAK-arrange for frameTitle to be initialized and the default file
3067 // name to be appended to basic window title
3068
3069 frameTitle = title;
3070 setTitle(null);
3071+ trySetLookAndFeel();
3072+
3073+ Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize();
3074+ this.setSize(screenSize.width * 80 / 100, screenSize.height * 80 / 100);
3075+ this.setLocationRelativeTo(null);
3076+ this.setMinimumSize(new Dimension(825, 480));
3077+
3078+ setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
3079+
3080+ //XXX: Moved appTab from creategui needs further refacotring
3081+ //kyrke 2018-05-20
3082+ appTab = new JTabbedPane();
3083+ getContentPane().add(appTab);
3084+ setChangeListenerOnTab(); // sets Tab properties
3085+
3086+
3087+ animator = new Animator();
3088+ Grid.enableGrid();
3089+
3090+ loadPrefrences();
3091+
3092+ buildMenus();
3093+
3094+ // Status bar...
3095+ statusBar = new StatusBar();
3096+ getContentPane().add(statusBar, BorderLayout.PAGE_END);
3097+
3098+ // Build menus
3099+ buildToolbar();
3100+
3101+ addWindowListener(new WindowAdapter() {
3102+ // Handler for window closing event
3103+ public void windowClosing(WindowEvent e) {
3104+ exitAction.actionPerformed(null);
3105+ }
3106+ });
3107+
3108+ this.setForeground(java.awt.Color.BLACK);
3109+
3110+ // Set GUI mode
3111+ setGUIMode(GUIMode.noNet);
3112+
3113+ //XXX 2018-05-23 kyrke: Moved from CreatGUI (static), needs further refactoring to seperate conserns
3114+ Verifyta.trySetup();
3115+ VerifyTAPN.trySetup();
3116+ VerifyTAPNDiscreteVerification.trySetup();
3117+ VerifyPN.trySetup();
3118+
3119+ }
3120+
3121+ private void trySetLookAndFeel() {
3122 try {
3123 // Set the Look and Feel native for the system.
3124- setLookAndFeel();
3125+ UIManager.setLookAndFeel(UIManager.getSystemLookAndFeelClassName());
3126+
3127+ //XXX Bug made us select non-native L&F for Windows, bug seems to be no longer present.
3128+// if(UIManager.getLookAndFeel().getName().equals("Windows")){
3129+// for (LookAndFeelInfo info : UIManager.getInstalledLookAndFeels()) {
3130+// if ("Nimbus".equals(info.getName())) {
3131+// UIManager.setLookAndFeel(info.getClassName());
3132+// UIManager.getLookAndFeelDefaults().put("List[Selected].textBackground", new Color(57, 105, 138));
3133+// UIManager.getLookAndFeelDefaults().put("List[Selected].textForeground", new Color(255,255,255));
3134+// UIManager.getLookAndFeelDefaults().put("List.background", new Color(255,255,255));
3135+//
3136+// break;
3137+// }
3138+// }
3139+// }
3140+
3141+ // Set enter to select focus button rather than default (makes ENTER selection key on all LAFs)
3142+ UIManager.put("Button.focusInputMap", new UIDefaults.LazyInputMap(new Object[]
3143+ {
3144+ "SPACE", "pressed",
3145+ "released SPACE", "released",
3146+ "ENTER", "pressed",
3147+ "released ENTER", "released"
3148+ }));
3149 UIManager.put("OptionPane.informationIcon", ResourceManager.infoIcon());
3150 UIManager.put("Slider.paintValue", false);
3151
3152 // 2010-05-07, Kenneth Yrke Joergensen:
3153 // If the native look and feel is GTK replace the useless open
3154- // dialog,
3155- // with a java-reimplementation.
3156+ // dialog, with a java-reimplementation.
3157
3158 if ("GTK look and feel".equals(UIManager.getLookAndFeel().getName())){
3159 try {
3160@@ -218,18 +291,17 @@
3161 Class.forName("com.google.code.gtkjfilechooser.ui.GtkFileChooserUI", false, this.getClass().getClassLoader());
3162 UIManager.put("FileChooserUI", "com.google.code.gtkjfilechooser.ui.GtkFileChooserUI");
3163 } catch (ClassNotFoundException exc){
3164- System.err.println("Error loading GtkFileChooserUI Look and Feel, using default jvm GTK look and feel instead");
3165- CreateGui.setUsingGTKFileBrowser(false);
3166+ Logger.log("Error loading GtkFileChooserUI Look and Feel, using default jvm GTK look and feel instead");
3167 }
3168
3169 }
3170
3171
3172 } catch (Exception exc) {
3173- System.err.println("Error loading L&F: " + exc);
3174+ Logger.log("Error loading L&F: " + exc);
3175 }
3176
3177- if (isMac()){
3178+ if (Platform.isMac()){
3179
3180 try{
3181 new SpecialMacHandler();
3182@@ -263,31 +335,6 @@
3183 }
3184
3185 this.setIconImage(new ImageIcon(Thread.currentThread().getContextClassLoader().getResource(CreateGui.imgPath + "icon.png")).getImage());
3186-
3187- Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize();
3188- this.setSize(screenSize.width * 80 / 100, screenSize.height * 80 / 100);
3189- this.setLocationRelativeTo(null);
3190- this.setMinimumSize(new Dimension(825, 480));
3191-
3192- setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
3193-
3194- loadPrefrences();
3195-
3196- buildMenus();
3197-
3198- // Status bar...
3199- statusBar = new StatusBar();
3200- getContentPane().add(statusBar, BorderLayout.PAGE_END);
3201-
3202- // Build menus
3203- buildToolbar();
3204-
3205- addWindowListener(new WindowHandler());
3206-
3207- this.setForeground(java.awt.Color.BLACK);
3208-
3209- // Set GUI mode
3210- setGUIMode(GUIMode.noNet);
3211 }
3212
3213 private void loadPrefrences() {
3214@@ -308,12 +355,12 @@
3215
3216 showToolTips = prefs.getShowToolTips();
3217
3218- if(CreateGui.showZeroToInfinityIntervals() != prefs.getShowZeroInfIntervals()){
3219- CreateGui.toggleShowZeroToInfinityIntervals();
3220+ if(showZeroToInfinityIntervals() != prefs.getShowZeroInfIntervals()){
3221+ toggleShowZeroToInfinityIntervals();
3222 }
3223
3224- if(CreateGui.showTokenAge() != prefs.getShowTokenAge()){
3225- CreateGui.toggleShowTokenAge();
3226+ if(showTokenAge() != prefs.getShowTokenAge()){
3227+ toggleShowTokenAge();
3228 }
3229
3230 Dimension dimension = prefs.getWindowSize();
3231@@ -323,287 +370,246 @@
3232
3233 }
3234
3235- private void setLookAndFeel() throws ClassNotFoundException, InstantiationException, IllegalAccessException, UnsupportedLookAndFeelException{
3236- UIManager.setLookAndFeel(UIManager.getSystemLookAndFeelClassName());
3237- if(UIManager.getLookAndFeel().getName().equals("Windows")){
3238- for (LookAndFeelInfo info : UIManager.getInstalledLookAndFeels()) {
3239- if ("Nimbus".equals(info.getName())) {
3240- UIManager.setLookAndFeel(info.getClassName());
3241- UIManager.getLookAndFeelDefaults().put("List[Selected].textBackground", new Color(57, 105, 138));
3242- UIManager.getLookAndFeelDefaults().put("List[Selected].textForeground", new Color(255,255,255));
3243- UIManager.getLookAndFeelDefaults().put("List.background", new Color(255,255,255));
3244-
3245- break;
3246- }
3247+ //XXX 2018-05-23 kyrke, moved from CreateGui, static method
3248+ //Needs further refactoring to seperate conserns
3249+ public void checkForUpdate(boolean forcecheck) {
3250+ final VersionChecker versionChecker = new VersionChecker();
3251+ if (versionChecker.checkForNewVersion(forcecheck)) {
3252+ StringBuffer message = new StringBuffer("There is a new version of TAPAAL available at www.tapaal.net.");
3253+ message.append("\n\nCurrent version: ");
3254+ message.append(TAPAAL.VERSION);
3255+ message.append("\nNew version: ");
3256+ message.append(versionChecker.getNewVersionNumber());
3257+ String changelog = versionChecker.getChangelog();
3258+ if (!changelog.equals("")){
3259+ message.append('\n');
3260+ message.append('\n');
3261+ message.append("Changelog:");
3262+ message.append('\n');
3263+ message.append(changelog);
3264 }
3265+ JOptionPane optionPane = new JOptionPane();
3266+ optionPane.setMessage(message.toString());
3267+ optionPane.setMessageType(JOptionPane.INFORMATION_MESSAGE);
3268+ JButton updateButton, laterButton, ignoreButton;
3269+ updateButton = new JButton("Update now");
3270+ updateButton.setMnemonic(KeyEvent.VK_C);
3271+ optionPane.add(updateButton);
3272+ laterButton = new JButton("Update later");
3273+ laterButton.setMnemonic(KeyEvent.VK_C);
3274+ optionPane.add(laterButton);
3275+ ignoreButton = new JButton("Ignore this update");
3276+ laterButton.setMnemonic(KeyEvent.VK_C);
3277+ optionPane.add(ignoreButton);
3278+
3279+ optionPane.setOptions(new Object[] {updateButton, laterButton, ignoreButton});
3280+
3281+
3282+ final JDialog dialog = optionPane.createDialog(null, "New Version of TAPAAL");
3283+ laterButton.addActionListener(new ActionListener() {
3284+ public void actionPerformed(ActionEvent e) {
3285+ Preferences.getInstance().setLatestVersion(null);
3286+ dialog.setVisible(false);
3287+ dialog.dispose ();
3288+ }
3289+ });
3290+ updateButton.addActionListener(new ActionListener() {
3291+ public void actionPerformed(ActionEvent e) {
3292+ Preferences.getInstance().setLatestVersion(null);
3293+ dialog.setVisible(false);
3294+ dialog.dispose();
3295+ pipe.gui.GuiFrame.showInBrowser("http://www.tapaal.net/download");
3296+ }
3297+ });
3298+ ignoreButton.addActionListener(new ActionListener() {
3299+ public void actionPerformed(ActionEvent e) {
3300+ Preferences.getInstance().setLatestVersion(versionChecker.getNewVersionNumber());
3301+ dialog.setVisible(false);
3302+ dialog.dispose ();
3303+ }
3304+ });
3305+
3306+ updateButton.requestFocusInWindow();
3307+ dialog.getRootPane().setDefaultButton(updateButton);
3308+ dialog.setVisible(true);
3309 }
3310-
3311- // Set enter to select focus button rather than default (makes ENTER selection key on all LAFs)
3312- UIManager.put("Button.focusInputMap", new UIDefaults.LazyInputMap(new Object[]
3313- {
3314- "SPACE", "pressed",
3315- "released SPACE", "released",
3316- "ENTER", "pressed",
3317- "released ENTER", "released"
3318- }));
3319 }
3320
3321 /**
3322- * This method does build the menus
3323- *
3324- * @author Dave Patterson - fixed problem on OSX due to invalid character in
3325- * URI caused by unescaped blank. The code changes one blank
3326- * character if it exists in the string version of the URL. This way
3327- * works safely in both OSX and Windows. I also added a
3328- * printStackTrace if there is an exception caught in the setup for
3329- * the "Example nets" folder.
3330- * @author Kenneth Yrke Joergensen <kenneth@yrke.dk>, 2011-06-28
3331- * Code cleanup, removed unused parts, Refactored help menu, Fixed
3332- * loading of Example Nets to work if we create a Jar.
3333+ * Build the menues and actions
3334 **/
3335 private void buildMenus() {
3336 menuBar = new JMenuBar();
3337
3338- JMenu fileMenu = new JMenu("File");
3339- fileMenu.setMnemonic('F');
3340-
3341 int shortcutkey = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask();
3342
3343- addMenuItem(fileMenu, createAction = new FileAction("New",
3344- "Create a new Petri net", "ctrl N"));
3345- createAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('N', shortcutkey));
3346-
3347- addMenuItem(fileMenu, openAction = new FileAction("Open", "Open",
3348- "ctrl O"));
3349- openAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('O', shortcutkey));
3350-
3351- addMenuItem(fileMenu, closeAction = new FileAction("Close",
3352- "Close the current tab", "ctrl W"));
3353- closeAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('W', shortcutkey));
3354- fileMenu.addSeparator();
3355-
3356- addMenuItem(fileMenu, saveAction = new FileAction("Save", "Save",
3357- "ctrl S"));
3358- saveAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('S', shortcutkey));
3359- addMenuItem(fileMenu, saveAsAction = new FileAction("Save as",
3360- "Save as...", null));
3361- saveAsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('S', (shortcutkey + InputEvent.SHIFT_MASK)));
3362-
3363-
3364- // Import menu
3365- importMenu = new JMenu("Import");
3366-
3367- importMenu.setIcon(new ImageIcon(Thread.currentThread()
3368- .getContextClassLoader().getResource(
3369- CreateGui.imgPath + "Export.png")));
3370- addMenuItem(importMenu, importPNMLAction = new FileAction("PNML untimed net",
3371- "Import an untimed net in the PNML format", "ctrl X"));
3372- importPNMLAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('X', shortcutkey));
3373-
3374- addMenuItem(importMenu, importSUMOAction = new FileAction("SUMO queries (.txt)",
3375- "Import SUMO queries in a plain text format",""));
3376- //importSUMOAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('R', shortcutkey));
3377-
3378- addMenuItem(importMenu, importXMLAction = new FileAction("XML queries (.xml)",
3379- "Import MCC queries in XML format", "ctrl R"));
3380- importXMLAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('R', shortcutkey));
3381-
3382- fileMenu.add(importMenu);
3383-
3384- // Export menu
3385- exportMenu = new JMenu("Export");
3386-
3387- exportMenu.setIcon(new ImageIcon(Thread.currentThread()
3388- .getContextClassLoader().getResource(
3389- CreateGui.imgPath + "Export.png")));
3390- addMenuItem(exportMenu, exportPNGAction = new FileAction("PNG",
3391- "Export the net to PNG format", "ctrl G"));
3392- exportPNGAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('G', shortcutkey));
3393- addMenuItem(exportMenu, exportPSAction = new FileAction("PostScript",
3394- "Export the net to PostScript format", "ctrl T"));
3395- exportPSAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('T', shortcutkey));
3396- addMenuItem(exportMenu, exportToTikZAction = new FileAction("TikZ",
3397- "Export the net to LaTex (TikZ) format", "ctrl L"));
3398- exportToTikZAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('L', shortcutkey));
3399- addMenuItem(exportMenu, exportToPNMLAction = new FileAction("PNML",
3400- "Export the net to PNML format", "ctrl D"));
3401- exportToPNMLAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('D', shortcutkey));
3402- addMenuItem(exportMenu, exportToXMLAction = new FileAction("XML Queries",
3403- "Export the queries to XML format", "ctrl H"));
3404- exportToXMLAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('H', shortcutkey));
3405- addMenuItem(exportMenu, exportBatchAction = new FileAction("Batch Export to PNML and XML Queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", "ctrl K"));
3406- exportBatchAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('K', shortcutkey));
3407-
3408- fileMenu.add(exportMenu);
3409-
3410- fileMenu.addSeparator();
3411- addMenuItem(fileMenu, printAction = new FileAction("Print", "Print",
3412- "ctrl P"));
3413- printAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('P', shortcutkey));
3414- fileMenu.addSeparator();
3415-
3416- // Example files menu
3417- try {
3418-
3419- /**
3420- * The next block loads the example nets as InputStream from the resources
3421- * Notice the check for if we are inside a jar file, as files inside a jar cant
3422- * be listed in the normal way.
3423- *
3424- * @author Kenneth Yrke Joergensen <kenneth@yrke.dk>, 2011-06-27
3425- */
3426-
3427- String[] nets = null;
3428-
3429- URL dirURL = Thread.currentThread().getContextClassLoader().getResource("resources/Example nets/");
3430- if (dirURL != null && dirURL.getProtocol().equals("file")) {
3431- /* A file path: easy enough */
3432- nets = new File(dirURL.toURI()).list();
3433- }
3434-
3435- if (dirURL == null) {
3436- /*
3437- * In case of a jar file, we can't actually find a directory.
3438- * Have to assume the same jar as clazz.
3439- */
3440- String me = this.getName().replace(".", "/")+".class";
3441- dirURL = Thread.currentThread().getContextClassLoader().getResource(me);
3442- }
3443-
3444- if (dirURL.getProtocol().equals("jar")) {
3445- /* A JAR path */
3446- String jarPath = dirURL.getPath().substring(5, dirURL.getPath().indexOf('!')); //strip out only the JAR file
3447- JarFile jar = new JarFile(URLDecoder.decode(jarPath, "UTF-8"));
3448- Enumeration<JarEntry> entries = jar.entries(); //gives ALL entries in jar
3449- Set<String> result = new HashSet<String>(); //avoid duplicates in case it is a subdirectory
3450- while(entries.hasMoreElements()) {
3451- String name = entries.nextElement().getName();
3452- if (name.startsWith("resources/Example nets/")) { //filter according to the path
3453- String entry = name.substring("resources/Example nets/".length());
3454- int checkSubdir = entry.indexOf('/');
3455- if (checkSubdir >= 0) {
3456- // if it is a subdirectory, we just return the directory name
3457- entry = entry.substring(0, checkSubdir);
3458- }
3459- result.add(entry);
3460- }
3461- }
3462- nets = result.toArray(new String[result.size()]);
3463- }
3464-
3465- Arrays.sort(nets, new Comparator<String>() {
3466- public int compare(String one, String two) {
3467-
3468- int toReturn = one.compareTo(two);
3469- // Special hack to get intro-example first
3470- if (one.equals("intro-example.xml")) {
3471- toReturn = -1;
3472- }
3473- if (two.equals("intro-example.xml")) {
3474- toReturn = 1;
3475- }
3476- return toReturn;
3477- }
3478- });
3479-
3480- // Oliver Haggarty - fixed code here so that if folder contains non
3481- // .xml file the Example x counter is not incremented when that file
3482- // is ignored
3483- if (nets.length > 0) {
3484- JMenu exampleMenu = new JMenu("Example nets");
3485- exampleMenu.setIcon(new ImageIcon(Thread.currentThread()
3486- .getContextClassLoader().getResource(
3487- CreateGui.imgPath + "Example.png")));
3488- int k = 0;
3489- for (int i = 0; i < nets.length; i++) {
3490- if (nets[i].toLowerCase().endsWith(".xml")) {
3491- //addMenuItem(exampleMenu, new ExampleFileAction(nets[i], (k < 10) ? "ctrl " + (k++) : null));
3492-
3493- ExampleFileAction tmp = new ExampleFileAction(nets[i], nets[i].replace(".xml", ""), null);
3494- if (k < 10) {
3495-
3496- //tmp.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyStroke.getKeyStroke(""+k).getKeyCode(), shortcutkey));
3497-
3498- }
3499- k++;
3500-
3501- addMenuItem(exampleMenu, tmp);
3502- }
3503- }
3504- fileMenu.add(exampleMenu);
3505- fileMenu.addSeparator();
3506- }
3507- } catch (Exception e) {
3508- Logger.log("Error getting example files:" + e);
3509- e.printStackTrace();
3510- }
3511- addMenuItem(fileMenu, exitAction = new FileAction("Exit",
3512- "Close the program", "ctrl Q"));
3513- exitAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('Q', shortcutkey));
3514+ menuBar.add(buildMenuFiles(shortcutkey));
3515+ menuBar.add(buildMenuEdit(shortcutkey));
3516+ menuBar.add(buildMenuView(shortcutkey));
3517+ menuBar.add(buildMenuDraw());
3518+ menuBar.add(buildMenuAnimation());
3519+ menuBar.add(buildMenuTools());
3520+ menuBar.add(buildMenuHelp());
3521+
3522+ setJMenuBar(menuBar);
3523+
3524+ }
3525+
3526+ private JMenu buildMenuEdit(int shortcutkey) {
3527
3528 /* Edit Menu */
3529 JMenu editMenu = new JMenu("Edit");
3530 editMenu.setMnemonic('E');
3531- addMenuItem(editMenu, undoAction = new EditAction("Undo",
3532- "Undo", "ctrl Z"));
3533- undoAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('Z', shortcutkey));
3534- addMenuItem(editMenu, redoAction = new EditAction("Redo",
3535- "Redo", "ctrl Y"));
3536- redoAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('Y', shortcutkey));
3537+ editMenu.add( undoAction = new GuiAction("Undo",
3538+ "Undo", KeyStroke.getKeyStroke('Z', shortcutkey)) {
3539+ @Override
3540+ public void actionPerformed(ActionEvent e) {
3541+ if (CreateGui.getApp().isEditionAllowed()) {
3542+ appView.getUndoManager().undo();
3543+ CreateGui.getCurrentTab().network().buildConstraints();
3544+ }
3545+ }
3546+ });
3547+
3548+
3549+ editMenu.add( redoAction = new GuiAction("Redo",
3550+ "Redo", KeyStroke.getKeyStroke('Y', shortcutkey)) {
3551+ @Override
3552+ public void actionPerformed(ActionEvent e) {
3553+ if (CreateGui.getApp().isEditionAllowed()) {
3554+ appView.getUndoManager().redo();
3555+ CreateGui.getCurrentTab().network().buildConstraints();
3556+ }
3557+ }
3558+ });
3559 editMenu.addSeparator();
3560
3561- addMenuItem(editMenu, deleteAction = new DeleteAction("Delete",
3562- "Delete selection", "DELETE"));
3563+ editMenu.add( deleteAction = new GuiAction("Delete", "Delete selection", "DELETE") {
3564+
3565+ @Override
3566+ public void actionPerformed(ActionEvent arg0) {
3567+ // check if queries need to be removed
3568+ ArrayList<PetriNetObject> selection = CreateGui.getDrawingSurface().getSelectionObject().getSelection();
3569+ Iterable<TAPNQuery> queries = ((TabContent) appTab.getSelectedComponent()).queries();
3570+ HashSet<TAPNQuery> queriesToDelete = new HashSet<TAPNQuery>();
3571+
3572+ boolean queriesAffected = false;
3573+ for (PetriNetObject pn : selection) {
3574+ if (pn instanceof TimedPlaceComponent) {
3575+ TimedPlaceComponent place = (TimedPlaceComponent)pn;
3576+ if(!place.underlyingPlace().isShared()){
3577+ for (TAPNQuery q : queries) {
3578+ if (q.getProperty().containsAtomicPropositionWithSpecificPlaceInTemplate(((LocalTimedPlace)place.underlyingPlace()).model().name(),place.underlyingPlace().name())) {
3579+ queriesAffected = true;
3580+ queriesToDelete.add(q);
3581+ }
3582+ }
3583+ }
3584+ } else if (pn instanceof TimedTransitionComponent){
3585+ TimedTransitionComponent transition = (TimedTransitionComponent)pn;
3586+ if(!transition.underlyingTransition().isShared()){
3587+ for (TAPNQuery q : queries) {
3588+ if (q.getProperty().containsAtomicPropositionWithSpecificTransitionInTemplate((transition.underlyingTransition()).model().name(),transition.underlyingTransition().name())) {
3589+ queriesAffected = true;
3590+ queriesToDelete.add(q);
3591+ }
3592+ }
3593+ }
3594+ }
3595+ }
3596+ StringBuilder s = new StringBuilder();
3597+ s.append("The following queries are associated with the currently selected objects:\n\n");
3598+ for (TAPNQuery q : queriesToDelete) {
3599+ s.append(q.getName());
3600+ s.append('\n');
3601+ }
3602+ s.append("\nAre you sure you want to remove the current selection and all associated queries?");
3603+
3604+ int choice = queriesAffected ? JOptionPane.showConfirmDialog(
3605+ CreateGui.getApp(), s.toString(), "Warning",
3606+ JOptionPane.YES_NO_OPTION, JOptionPane.QUESTION_MESSAGE)
3607+ : JOptionPane.YES_OPTION;
3608+
3609+ if (choice == JOptionPane.YES_OPTION) {
3610+ appView.getUndoManager().newEdit(); // new "transaction""
3611+ if (queriesAffected) {
3612+ TabContent currentTab = CreateGui.getCurrentTab();
3613+ for (TAPNQuery q : queriesToDelete) {
3614+ Command cmd = new DeleteQueriesCommand(currentTab, Arrays.asList(q));
3615+ cmd.redo();
3616+ appView.getUndoManager().addEdit(cmd);
3617+ }
3618+ }
3619+
3620+ appView.getUndoManager().deleteSelection(appView.getSelectionObject().getSelection());
3621+ appView.getSelectionObject().deleteSelection();
3622+ appView.repaint();
3623+ CreateGui.getCurrentTab().network().buildConstraints();
3624+ }
3625+
3626+ }
3627+
3628+ });
3629
3630 // Bind delete to backspace also
3631 editMenu.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(
3632 KeyStroke.getKeyStroke("BACK_SPACE"), "Delete");
3633 editMenu.getActionMap().put("Delete", deleteAction);
3634-
3635+
3636 editMenu.addSeparator();
3637
3638- addMenuItem(editMenu, selectAllAction = new SelectAllAction("Select all",
3639- "Select all components", "ctrl A"));
3640
3641- editMenu.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(
3642- KeyStroke.getKeyStroke('A', shortcutkey), "SelectAll");
3643+ editMenu.add(selectAllAction = new GuiAction("Select all", "Select all components", KeyStroke.getKeyStroke('A', shortcutkey )) {
3644+ @Override
3645+ public void actionPerformed(ActionEvent e) {
3646+ CreateGui.getDrawingSurface().getSelectionObject().selectAll();
3647+ }
3648+ });
3649+ editMenu.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(KeyStroke.getKeyStroke('A', shortcutkey), "SelectAll");
3650 editMenu.getActionMap().put("SelectAll", selectAllAction);
3651
3652+ return editMenu;
3653+ }
3654+
3655+ private JMenu buildMenuDraw() {
3656 /* Draw menu */
3657 JMenu drawMenu = new JMenu("Draw");
3658 drawMenu.setMnemonic('D');
3659- addMenuItem(drawMenu, selectAction = new TypeAction("Select",
3660+ drawMenu.add( selectAction = new TypeAction("Select",
3661 ElementType.SELECT, "Select components (S)", "S", true));
3662 drawMenu.addSeparator();
3663
3664- addMenuItem(drawMenu, timedPlaceAction = new TypeAction("Place",
3665+ drawMenu.add( timedPlaceAction = new TypeAction("Place",
3666 ElementType.TAPNPLACE, "Add a place (P)", "P", true));
3667
3668- addMenuItem(drawMenu, transAction = new TypeAction("Transition",
3669+ drawMenu.add( transAction = new TypeAction("Transition",
3670 ElementType.TAPNTRANS, "Add a transition (T)", "T", true));
3671
3672- addMenuItem(drawMenu, timedArcAction = new TypeAction("Arc",
3673+ drawMenu.add( timedArcAction = new TypeAction("Arc",
3674 ElementType.TAPNARC, "Add an arc (A)", "A", true));
3675
3676- addMenuItem(drawMenu, transportArcAction = new TypeAction(
3677+ drawMenu.add( transportArcAction = new TypeAction(
3678 "Transport arc", ElementType.TRANSPORTARC, "Add a transport arc (R)", "R",
3679 true));
3680
3681- addMenuItem(drawMenu, inhibarcAction = new TypeAction("Inhibitor arc",
3682+ drawMenu.add( inhibarcAction = new TypeAction("Inhibitor arc",
3683 ElementType.TAPNINHIBITOR_ARC, "Add an inhibitor arc (I)", "I", true));
3684
3685- addMenuItem(drawMenu, annotationAction = new TypeAction("Annotation",
3686+ drawMenu.add(annotationAction = new TypeAction("Annotation",
3687 ElementType.ANNOTATION, "Add an annotation (N)", "N", true));
3688
3689 drawMenu.addSeparator();
3690
3691- addMenuItem(drawMenu, tokenAction = new TypeAction("Add token",
3692+ drawMenu.add( tokenAction = new TypeAction("Add token",
3693 ElementType.ADDTOKEN, "Add a token (+)", "typed +", true));
3694
3695- addMenuItem(drawMenu, deleteTokenAction = new TypeAction(
3696+ drawMenu.add( deleteTokenAction = new TypeAction(
3697 "Delete token", ElementType.DELTOKEN, "Delete a token (-)", "typed -",
3698 true));
3699+ return drawMenu;
3700+ }
3701
3702+ private JMenu buildMenuView(int shortcutkey) {
3703 /* ViewMenu */
3704 JMenu viewMenu = new JMenu("View");
3705 viewMenu.setMnemonic('V');
3706@@ -612,224 +618,364 @@
3707 zoomMenu.setIcon(new ImageIcon(Thread.currentThread()
3708 .getContextClassLoader().getResource(
3709 CreateGui.imgPath + "Zoom.png")));
3710+
3711 addZoomMenuItems(zoomMenu);
3712
3713- addMenuItem(viewMenu, zoomInAction = new ZoomAction("Zoom in",
3714- "Zoom in by 10% ", "ctrl J"));
3715- zoomInAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyStroke.getKeyStroke("J").getKeyCode(), shortcutkey));
3716+ viewMenu.add( zoomInAction = new GuiAction("Zoom in",
3717+ "Zoom in by 10% ", KeyStroke.getKeyStroke('J', shortcutkey)) {
3718+ @Override
3719+ public void actionPerformed(ActionEvent e) {
3720+ boolean didZoom = appView.getZoomController().zoomIn();
3721+ if (didZoom) {
3722+ updateZoomCombo();
3723+ appView.zoomToMidPoint(); //Do Zoom
3724+ }
3725+ }
3726+ });
3727
3728- addMenuItem(viewMenu, zoomOutAction = new ZoomAction("Zoom out",
3729- "Zoom out by 10% ", "ctrl K"));
3730- zoomOutAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyStroke.getKeyStroke("K").getKeyCode(), shortcutkey));
3731+ viewMenu.add( zoomOutAction = new GuiAction("Zoom out",
3732+ "Zoom out by 10% ", KeyStroke.getKeyStroke('K', shortcutkey)) {
3733+ @Override
3734+ public void actionPerformed(ActionEvent e) {
3735+ boolean didZoom = appView.getZoomController().zoomOut();
3736+ if (didZoom) {
3737+ updateZoomCombo();
3738+ appView.zoomToMidPoint(); //Do Zoom
3739+ }
3740+ }
3741+ });
3742 viewMenu.add(zoomMenu);
3743
3744 viewMenu.addSeparator();
3745
3746- addMenuItem(viewMenu, incSpacingAction = new SpacingAction("Increase node spacing",
3747- "Increase spacing by 20% ", null));
3748- incSpacingAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyStroke.getKeyStroke("U").getKeyCode(), shortcutkey));
3749-
3750- addMenuItem(viewMenu, decSpacingAction = new SpacingAction("Decrease node spacing",
3751- "Decrease spacing by 20% ", null));
3752- decSpacingAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke("shift U"));
3753-
3754-
3755- viewMenu.addSeparator();
3756-
3757- addMenuItem(viewMenu, toggleGrid = new GridAction("Cycle grid",
3758- "Change the grid size", "G"));
3759-
3760- viewMenu.addSeparator();
3761-
3762- addCheckboxMenuItem(viewMenu, showComponents, showComponentsAction = new ViewAction("Display components",
3763- 453243, "Show/hide the list of components.", "ctrl 1", true),
3764- showComponentsCheckBox = new JCheckBoxMenuItem());
3765- showComponentsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('1', shortcutkey));
3766-
3767- addCheckboxMenuItem(viewMenu, showQueries, showQueriesAction = new ViewAction("Display queries",
3768- 453244, "Show/hide verification queries.", "ctrl 2", true),
3769- showQueriesCheckBox= new JCheckBoxMenuItem());
3770- showQueriesAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('2', shortcutkey));
3771-
3772- addCheckboxMenuItem(viewMenu, showConstants, showConstantsAction = new ViewAction("Display constants",
3773- 453245, "Show/hide global constants.", "ctrl 3", true),
3774- showConstantsCheckBox = new JCheckBoxMenuItem());
3775- showConstantsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('3', shortcutkey));
3776-
3777- addCheckboxMenuItem(viewMenu, showEnabledTransitions, showEnabledTransitionsAction = new ViewAction("Display enabled transitions",
3778- 453247, "Show/hide the list of enabled transitions","ctrl 4",true),
3779- showEnabledTransitionsCheckBox = new JCheckBoxMenuItem());
3780- showEnabledTransitionsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('4', shortcutkey));
3781-
3782- addCheckboxMenuItem(viewMenu, showDelayEnabledTransitions, showDelayEnabledTransitionsAction = new ViewAction("Display future-enabled transitions",
3783- 453247, "Highlight transitions which can be enabled after a delay","ctrl 5",true),
3784- showDelayEnabledTransitionsCheckBox = new JCheckBoxMenuItem());
3785- showDelayEnabledTransitionsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('5', shortcutkey));
3786-
3787- addCheckboxMenuItem(viewMenu, CreateGui.showZeroToInfinityIntervals(), showZeroToInfinityIntervalsAction = new ViewAction("Display intervals [0,inf)",
3788- 453246, "Show/hide intervals [0,inf) that do not restrict transition firing in any way.","ctrl 6",true),
3789- showZeroToInfinityIntervalsCheckBox = new JCheckBoxMenuItem());
3790- showZeroToInfinityIntervalsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('6', shortcutkey));
3791-
3792- addCheckboxMenuItem(viewMenu, showToolTips, showToolTipsAction = new ViewAction("Display tool tips",
3793- 453246, "Show/hide tool tips when mouse is over an element","ctrl 7",true),
3794- showToolTipsCheckBox = new JCheckBoxMenuItem());
3795- showToolTipsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('7', shortcutkey));
3796-
3797- addCheckboxMenuItem(viewMenu, CreateGui.showTokenAge(), showTokenAgeAction = new ViewAction("Display token age",
3798- 453246, "Show/hide displaying the token age 0.0 (when hidden the age 0.0 is drawn as a dot)","ctrl 8",true),
3799- showTokenAgeCheckBox = new JCheckBoxMenuItem());
3800- showTokenAgeAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('8', shortcutkey));
3801-
3802- viewMenu.addSeparator();
3803-
3804- addMenuItem(viewMenu, showSimpleWorkspaceAction = new ViewAction("Show simple workspace", 453249, "Show only the most important panels", "", false));
3805- addMenuItem(viewMenu, showAdvancedWorkspaceAction = new ViewAction("Show advanced workspace", 453248, "Show all panels", "", false));
3806- addMenuItem(viewMenu, saveWorkSpaceAction = new ViewAction("Save workspace", 453250, "Save the current workspace as the default one", "", false));
3807-
3808+ viewMenu.add(incSpacingAction = new GuiAction("Increase node spacing", "Increase spacing by 20% ",
3809+ KeyStroke.getKeyStroke('U', shortcutkey)) {
3810+ public void actionPerformed(ActionEvent arg0) {
3811+ double factor = 1.25;
3812+ changeSpacing(factor);
3813+ appView.getUndoManager().addNewEdit(new ChangeSpacingEdit(factor));
3814+ }
3815+ });
3816+
3817+ viewMenu.add(decSpacingAction = new GuiAction("Decrease node spacing", "Decrease spacing by 20% ",
3818+ KeyStroke.getKeyStroke("shift U")) {
3819+ public void actionPerformed(ActionEvent arg0) {
3820+ double factor = 0.8;
3821+ changeSpacing(factor);
3822+ appView.getUndoManager().addNewEdit(new ChangeSpacingEdit(factor));
3823+ }
3824+ });
3825+
3826+
3827+
3828+ viewMenu.addSeparator();
3829+
3830+ viewMenu.add( toggleGrid = new GuiAction("Cycle grid",
3831+ "Change the grid size", "G") {
3832+ public void actionPerformed(ActionEvent arg0) {
3833+ Grid.increment();
3834+ repaint();
3835+ }
3836+ });
3837+
3838+
3839+ viewMenu.addSeparator();
3840+
3841+ showComponentsAction = new GuiAction("Display components", "Show/hide the list of components.",
3842+ KeyStroke.getKeyStroke('1', shortcutkey), true) {
3843+ @Override
3844+ public void actionPerformed(ActionEvent e) {
3845+ toggleComponents();
3846+ }
3847+ };
3848+ addCheckboxMenuItem(viewMenu, showComponents, showComponentsAction);
3849+
3850+ showQueriesAction = new GuiAction("Display queries", "Show/hide verification queries.",
3851+ KeyStroke.getKeyStroke('2', shortcutkey), true) {
3852+ @Override
3853+ public void actionPerformed(ActionEvent e) {
3854+ toggleQueries();
3855+ }
3856+ };
3857+ addCheckboxMenuItem(viewMenu, showQueries, showQueriesAction);
3858+
3859+ showConstantsAction = new GuiAction("Display constants", "Show/hide global constants.",
3860+ KeyStroke.getKeyStroke('3', shortcutkey), true) {
3861+ @Override
3862+ public void actionPerformed(ActionEvent e) {
3863+ toggleConstants();
3864+ }
3865+ };
3866+ addCheckboxMenuItem(viewMenu, showConstants, showConstantsAction);
3867+
3868+ showEnabledTransitionsAction = new GuiAction("Display enabled transitions",
3869+ "Show/hide the list of enabled transitions", KeyStroke.getKeyStroke('4', shortcutkey), true) {
3870+ @Override
3871+ public void actionPerformed(ActionEvent e) {
3872+ toggleEnabledTransitionsList();
3873+ }
3874+ };
3875+ addCheckboxMenuItem(viewMenu, showEnabledTransitions, showEnabledTransitionsAction);
3876+
3877+ showDelayEnabledTransitionsAction = new GuiAction("Display future-enabled transitions",
3878+ "Highlight transitions which can be enabled after a delay", KeyStroke.getKeyStroke('5', shortcutkey),
3879+ true) {
3880+ @Override
3881+ public void actionPerformed(ActionEvent e) {
3882+ toggleDelayEnabledTransitions();
3883+ }
3884+ };
3885+ addCheckboxMenuItem(viewMenu, showDelayEnabledTransitions, showDelayEnabledTransitionsAction);
3886+
3887+ showZeroToInfinityIntervalsAction = new GuiAction("Display intervals [0,inf)",
3888+ "Show/hide intervals [0,inf) that do not restrict transition firing in any way.",
3889+ KeyStroke.getKeyStroke('6', shortcutkey), true) {
3890+ @Override
3891+ public void actionPerformed(ActionEvent e) {
3892+ toggleZeroToInfinityIntervals();
3893+ }
3894+ };
3895+ showZeroToInfinityIntervalsCheckBox = addCheckboxMenuItem(viewMenu, showZeroToInfinityIntervals(),
3896+ showZeroToInfinityIntervalsAction);
3897+
3898+ showToolTipsAction = new GuiAction("Display tool tips", "Show/hide tool tips when mouse is over an element",
3899+ KeyStroke.getKeyStroke('7', shortcutkey), true) {
3900+ @Override
3901+ public void actionPerformed(ActionEvent e) {
3902+ toggleToolTips();
3903+ }
3904+ };
3905+ addCheckboxMenuItem(viewMenu, showToolTips, showToolTipsAction);
3906+
3907+ showTokenAgeAction = new GuiAction("Display token age",
3908+ "Show/hide displaying the token age 0.0 (when hidden the age 0.0 is drawn as a dot)",
3909+ KeyStroke.getKeyStroke('8', shortcutkey), true) {
3910+ @Override
3911+ public void actionPerformed(ActionEvent e) {
3912+ toggleTokenAge();
3913+ }
3914+ };
3915+ showTokenAgeCheckBox = addCheckboxMenuItem(viewMenu, showTokenAge(), showTokenAgeAction);
3916+
3917+ viewMenu.addSeparator();
3918+
3919+ viewMenu.add( showSimpleWorkspaceAction = new GuiAction("Show simple workspace", "Show only the most important panels", false) {
3920+ @Override
3921+ public void actionPerformed(ActionEvent e) {
3922+ showAdvancedWorkspace(false);
3923+ }
3924+ });
3925+ viewMenu.add( showAdvancedWorkspaceAction = new GuiAction("Show advanced workspace", "Show all panels", false) {
3926+ @Override
3927+ public void actionPerformed(ActionEvent e) {
3928+ showAdvancedWorkspace(true);
3929+ }
3930+ });
3931+ viewMenu.add( saveWorkSpaceAction = new GuiAction("Save workspace", "Save the current workspace as the default one", false) {
3932+ @Override
3933+ public void actionPerformed(ActionEvent e) {
3934+ saveWorkspace();
3935+ }
3936+ });
3937+ return viewMenu;
3938+ }
3939+
3940+ private JMenu buildMenuAnimation() {
3941 /* Simulator */
3942 JMenu animateMenu = new JMenu("Simulator");
3943 animateMenu.setMnemonic('A');
3944- addMenuItem(animateMenu, startAction = new AnimateAction(
3945- "Simulation mode", ElementType.START, "Toggle simulation mode (M)",
3946- "M", true));
3947- addMenuItem(animateMenu, stepbackwardAction = new AnimateAction("Step backward",
3948- ElementType.STEPBACKWARD, "Step backward", "pressed LEFT"));
3949- addMenuItem(animateMenu,
3950- stepforwardAction = new AnimateAction("Step forward",
3951- ElementType.STEPFORWARD, "Step forward", "pressed RIGHT"));
3952-
3953- addMenuItem(animateMenu, timeAction = new AnimateAction("Delay one time unit",
3954- ElementType.TIMEPASS, "Let time pass one time unit", "W"));
3955-
3956- addMenuItem(animateMenu, delayFireAction = new AnimateAction("Delay and fire",
3957- ElementType.DELAYFIRE, "Delay and fire selected transition", "F"));
3958-
3959- addMenuItem(animateMenu, prevcomponentAction = new AnimateAction("Previous component",
3960- ElementType.PREVCOMPONENT, "Previous component", "pressed UP"));
3961-
3962- addMenuItem(animateMenu, nextcomponentAction = new AnimateAction("Next component",
3963- ElementType.NEXTCOMPONENT, "Next component", "pressed DOWN"));
3964+ animateMenu.add( startAction = new GuiAction(
3965+ "Simulation mode", "Toggle simulation mode (M)",
3966+ "M", true) {
3967+ @Override
3968+ public void actionPerformed(ActionEvent e) {
3969+ toggleAnimationMode();
3970+ }
3971+ });
3972+
3973+
3974+ animateMenu.add( stepbackwardAction = new GuiAction("Step backward",
3975+ "Step backward", "pressed LEFT") {
3976+ @Override
3977+ public void actionPerformed(ActionEvent e) {
3978+ CreateGui.getCurrentTab().getAnimationHistory().stepBackwards();
3979+ getAnimator().stepBack();
3980+ updateMouseOverInformation();
3981+ CreateGui.getCurrentTab().getAnimationController().setAnimationButtonsEnabled();
3982+ }
3983+ });
3984+ animateMenu.add(
3985+ stepforwardAction = new GuiAction("Step forward", "Step forward", "pressed RIGHT") {
3986+ @Override
3987+ public void actionPerformed(ActionEvent e) {
3988+ CreateGui.getCurrentTab().getAnimationHistory().stepForward();
3989+ getAnimator().stepForward();
3990+ updateMouseOverInformation();
3991+ CreateGui.getCurrentTab().getAnimationController().setAnimationButtonsEnabled();
3992+ }
3993+ });
3994+
3995+ animateMenu.add( timeAction = new GuiAction("Delay one time unit",
3996+ "Let time pass one time unit", "W") {
3997+ @Override
3998+ public void actionPerformed(ActionEvent e) {
3999+ getAnimator().letTimePass(BigDecimal.ONE);
4000+ CreateGui.getCurrentTab().getAnimationController().setAnimationButtonsEnabled();
4001+ updateMouseOverInformation();
4002+ }
4003+ });
4004+
4005+ animateMenu.add( delayFireAction = new GuiAction("Delay and fire",
4006+ "Delay and fire selected transition", "F") {
4007+ @Override
4008+ public void actionPerformed(ActionEvent e) {
4009+ CreateGui.getCurrentTab().getTransitionFireingComponent().fireSelectedTransition();
4010+ CreateGui.getCurrentTab().getAnimationController().setAnimationButtonsEnabled();
4011+ updateMouseOverInformation();
4012+ }
4013+ });
4014+
4015+ animateMenu.add( prevcomponentAction = new GuiAction("Previous component",
4016+ "Previous component", "pressed UP") {
4017+ @Override
4018+ public void actionPerformed(ActionEvent e) {
4019+ CreateGui.getCurrentTab().getTemplateExplorer().selectPrevious();
4020+ }
4021+ });
4022+
4023+ animateMenu.add( nextcomponentAction = new GuiAction("Next component",
4024+ "Next component", "pressed DOWN") {
4025+ @Override
4026+ public void actionPerformed(ActionEvent e) {
4027+ CreateGui.getCurrentTab().getTemplateExplorer().selectNext();
4028+ }
4029+ });
4030
4031 animateMenu.addSeparator();
4032
4033- addMenuItem(animateMenu, exportTraceAction = new FileAction("Export trace",
4034- "Export the current trace",""));
4035- addMenuItem(animateMenu, importTraceAction = new FileAction("Import trace",
4036- "Import trace to simulator",""));
4037-
4038- /*
4039- * addMenuItem(animateMenu, randomAction = new AnimateAction("Random",
4040- * Pipe.RANDOM, "Randomly fire a transition", "typed 5"));
4041- * addMenuItem(animateMenu, randomAnimateAction = new
4042- * AnimateAction("Simulate", Pipe.ANIMATE,
4043- * "Randomly fire a number of transitions", "typed 7",true));
4044- */
4045- randomAction = new AnimateAction("Random", ElementType.RANDOM,
4046- "Randomly fire a transition", "typed 5");
4047- randomAnimateAction = new AnimateAction("Simulate", ElementType.ANIMATE,
4048- "Randomly fire a number of transitions", "typed 7", true);
4049-
4050-
4051- /* The help part */
4052+ animateMenu.add( exportTraceAction = new GuiAction("Export trace",
4053+ "Export the current trace","") {
4054+ public void actionPerformed(ActionEvent arg0) {
4055+ TraceImportExport.exportTrace();
4056+ }
4057+ });
4058+ animateMenu.add( importTraceAction = new GuiAction("Import trace",
4059+ "Import trace to simulator",""){
4060+ public void actionPerformed(ActionEvent arg0) {
4061+ TraceImportExport.importTrace();
4062+ }
4063+ });
4064+
4065+
4066+ return animateMenu;
4067+ }
4068+
4069+ private JMenu buildMenuHelp() {
4070 JMenu helpMenu = new JMenu("Help");
4071 helpMenu.setMnemonic('H');
4072
4073- addMenuItem(helpMenu, showHomepage = new HelpAction("Visit TAPAAL home",
4074- 453257, "Visit the TAPAAL homepage", "_"));
4075-
4076- addMenuItem(helpMenu, checkUpdate = new HelpAction("Check for updates",
4077- 463257, "Check if there is a new version of TAPAAL", "_"));
4078-
4079- helpMenu.addSeparator();
4080-
4081- addMenuItem(helpMenu, showFAQAction = new HelpAction("Show FAQ",
4082- 454256, "See TAPAAL frequently asked questions", "_"));
4083- addMenuItem(helpMenu, showAskQuestionAction = new HelpAction("Ask a question",
4084- 453256, "Ask a question about TAPAAL", "_"));
4085- addMenuItem(helpMenu, showReportBugAction = new HelpAction("Report bug",
4086- 453254, "Report a bug in TAPAAL", "_"));
4087-
4088- helpMenu.addSeparator();
4089-
4090- addMenuItem(helpMenu, showAboutAction = new HelpAction("About",
4091- 453246, "Show the About menu", "_"));
4092-
4093- menuBar.add(fileMenu);
4094- menuBar.add(editMenu);
4095- menuBar.add(viewMenu);
4096- menuBar.add(drawMenu);
4097- menuBar.add(animateMenu);
4098- menuBar.add(buildToolsMenu());
4099- menuBar.add(helpMenu);
4100-
4101- setJMenuBar(menuBar);
4102-
4103+ helpMenu.add(showHomepage = new GuiAction("Visit TAPAAL home", "Visit the TAPAAL homepage") {
4104+ public void actionPerformed(ActionEvent arg0) {
4105+ showInBrowser("http://www.tapaal.net");
4106+ }
4107+ });
4108+
4109+ helpMenu.add(checkUpdate = new GuiAction("Check for updates", "Check if there is a new version of TAPAAL") {
4110+ public void actionPerformed(ActionEvent arg0) {
4111+ checkForUpdate(true);
4112+ }
4113+ });
4114+
4115+ helpMenu.addSeparator();
4116+
4117+ helpMenu.add(showFAQAction = new GuiAction("Show FAQ", "See TAPAAL frequently asked questions") {
4118+ public void actionPerformed(ActionEvent arg0) {
4119+ showInBrowser("https://answers.launchpad.net/tapaal/+faqs");
4120+ }
4121+ });
4122+ helpMenu.add(showAskQuestionAction = new GuiAction("Ask a question", "Ask a question about TAPAAL") {
4123+ public void actionPerformed(ActionEvent arg0) {
4124+ showInBrowser("https://answers.launchpad.net/tapaal/+addquestion");
4125+ }
4126+ });
4127+ helpMenu.add(showReportBugAction = new GuiAction("Report bug", "Report a bug in TAPAAL") {
4128+ public void actionPerformed(ActionEvent arg0) {
4129+ showInBrowser("https://bugs.launchpad.net/tapaal/+filebug");
4130+ }
4131+ });
4132+
4133+ helpMenu.addSeparator();
4134+
4135+ helpMenu.add(showAboutAction = new GuiAction("About", "Show the About menu") {
4136+ public void actionPerformed(ActionEvent arg0) {
4137+ showAbout();
4138+ }
4139+ });
4140+ return helpMenu;
4141 }
4142
4143- private JMenu buildToolsMenu() {
4144+
4145+
4146+ private JMenu buildMenuTools() {
4147 JMenu toolsMenu = new JMenu("Tools");
4148 toolsMenu.setMnemonic('t');
4149
4150 int shortcutkey = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask();
4151
4152- verification = new JMenuItem(verifyAction = new ToolAction("Verify query","Verifies the currently selected query",KeyStroke.getKeyStroke(KeyEvent.VK_M, shortcutkey)));
4153- verification.setMnemonic('m');
4154- verification.addActionListener(new ActionListener() {
4155+ verifyAction = new GuiAction("Verify query", "Verifies the currently selected query", KeyStroke.getKeyStroke(KeyEvent.VK_M, shortcutkey)) {
4156 public void actionPerformed(ActionEvent arg0) {
4157- CreateGui.getCurrentTab().verifySelectedQuery();
4158+ CreateGui.getCurrentTab().verifySelectedQuery();
4159 }
4160- });
4161- toolsMenu.add(verification);
4162- statistics = new JMenuItem(netStatisticsAction = new ToolAction("Net statistics", "Shows information about the number of transitions, places, arcs, etc.",KeyStroke.getKeyStroke(KeyEvent.VK_I, shortcutkey)));
4163- statistics.setMnemonic('i');
4164- statistics.addActionListener(new ActionListener() {
4165- public void actionPerformed(ActionEvent arg0) {
4166+ };
4167+ toolsMenu.add(verifyAction).setMnemonic('m');
4168+
4169+ netStatisticsAction = new GuiAction("Net statistics", "Shows information about the number of transitions, places, arcs, etc.", KeyStroke.getKeyStroke(KeyEvent.VK_I, shortcutkey)) {
4170+ @Override
4171+ public void actionPerformed(ActionEvent e) {
4172 StatisticsPanel.showStatisticsPanel();
4173 }
4174- });
4175- toolsMenu.add(statistics);
4176+ };
4177+ toolsMenu.add(netStatisticsAction).setMnemonic('i');
4178
4179
4180 //JMenuItem batchProcessing = new JMenuItem("Batch processing");
4181- JMenuItem batchProcessing = new JMenuItem(batchProcessingAction = new ToolAction("Batch processing", "Batch verification of multiple nets and queries",KeyStroke.getKeyStroke(KeyEvent.VK_B, shortcutkey)));
4182- batchProcessing.setMnemonic('b');
4183- batchProcessing.addActionListener(new ActionListener() {
4184- public void actionPerformed(ActionEvent arg0) {
4185+ JMenuItem batchProcessing = new JMenuItem(batchProcessingAction = new GuiAction("Batch processing", "Batch verification of multiple nets and queries", KeyStroke.getKeyStroke(KeyEvent.VK_B, shortcutkey)) {
4186+ @Override
4187+ public void actionPerformed(ActionEvent e) {
4188 if(checkForSaveAll()){
4189 BatchProcessingDialog.showBatchProcessingDialog(new JList(new DefaultListModel()));
4190 }
4191 }
4192 });
4193+ batchProcessing.setMnemonic('b');
4194 toolsMenu.add(batchProcessing);
4195
4196- JMenuItem workflowDialog = new JMenuItem(workflowDialogAction = new ToolAction("Workflow analysis", "Analyse net as a TAWFN", KeyStroke.getKeyStroke(KeyEvent.VK_F, shortcutkey)));
4197+ JMenuItem workflowDialog = new JMenuItem(workflowDialogAction = new GuiAction("Workflow analysis", "Analyse net as a TAWFN", KeyStroke.getKeyStroke(KeyEvent.VK_F, shortcutkey)) {
4198+ @Override
4199+ public void actionPerformed(ActionEvent e) {
4200+ WorkflowDialog.showDialog();
4201+ }
4202+ });
4203 workflowDialog.setMnemonic('f');
4204- workflowDialog.addActionListener(new ActionListener() {
4205- public void actionPerformed(ActionEvent arg0) {
4206- WorkflowDialog.showDialog();
4207- }
4208- });
4209 toolsMenu.add(workflowDialog);
4210
4211 //Stip off timing information
4212- JMenuItem stripTimeDialog = new JMenuItem(stripTimeDialogAction = new ToolAction("Remove timing information", "Remove all timing information from the net in the active tab and open it as a P/T net in a new tab.", KeyStroke.getKeyStroke(KeyEvent.VK_E, shortcutkey)));
4213- stripTimeDialog.setMnemonic('e');
4214- stripTimeDialog.addActionListener(new ActionListener() {
4215- public void actionPerformed(ActionEvent arg0) {
4216+ JMenuItem stripTimeDialog = new JMenuItem(stripTimeDialogAction = new GuiAction("Remove timing information", "Remove all timing information from the net in the active tab and open it as a P/T net in a new tab.", KeyStroke.getKeyStroke(KeyEvent.VK_E, shortcutkey)) {
4217+ @Override
4218+ public void actionPerformed(ActionEvent e) {
4219 duplicateTab((TabContent) appTab.getSelectedComponent());
4220 convertToUntimedTab((TabContent) appTab.getSelectedComponent());
4221 }
4222 });
4223+ stripTimeDialog.setMnemonic('e');
4224 toolsMenu.add(stripTimeDialog);
4225
4226 toolsMenu.addSeparator();
4227
4228- //JMenuItem engineSelection = new JMenuItem("Verification engines");
4229- JMenuItem engineSelection = new JMenuItem(engineSelectionAction = new ToolAction("Engine selection", "View and modify the location of verification engines",null));
4230- engineSelection.addActionListener(new ActionListener() {
4231- public void actionPerformed(ActionEvent arg0) {
4232- new EngineDialogPanel().showDialog();
4233+ JMenuItem engineSelection = new JMenuItem(engineSelectionAction = new GuiAction("Engine selection", "View and modify the location of verification engines") {
4234+ @Override
4235+ public void actionPerformed(ActionEvent e) {
4236+ new EngineDialogPanel().showDialog();
4237 }
4238 });
4239 toolsMenu.add(engineSelection);
4240@@ -852,7 +998,7 @@
4241 return toolsMenu;
4242 }
4243
4244- public void showAdvancedWorkspace(boolean advanced){
4245+ private void showAdvancedWorkspace(boolean advanced){
4246 QueryDialog.setAdvancedView(advanced);
4247 showComponents(advanced);
4248 showConstants(advanced);
4249@@ -862,10 +1008,10 @@
4250 showEnabledTransitionsList(true);
4251 showToolTips(true);
4252 CreateGui.getCurrentTab().setResizeingDefault();
4253- if(!CreateGui.showZeroToInfinityIntervals()){
4254+ if(!showZeroToInfinityIntervals()){
4255 showZeroToInfinityIntervalsCheckBox.doClick();
4256 }
4257- if(!CreateGui.showTokenAge()){
4258+ if(!showTokenAge()){
4259 showTokenAgeCheckBox.doClick();
4260 }
4261 //Delay-enabled Transitions
4262@@ -875,7 +1021,7 @@
4263 DelayEnabledTransitionControl.getInstance().setRandomTransitionMode(false);
4264 }
4265
4266- public void saveWorkspace(){
4267+ private void saveWorkspace(){
4268 Preferences prefs = Preferences.getInstance();
4269
4270 prefs.setAdvancedQueryView(QueryDialog.getAdvancedView());
4271@@ -889,7 +1035,7 @@
4272
4273 prefs.setShowEnabledTrasitions(showEnabledTransitions);
4274 prefs.setShowDelayEnabledTransitions(showDelayEnabledTransitions);
4275- prefs.setShowTokenAge(CreateGui.showTokenAge());
4276+ prefs.setShowTokenAge(showTokenAge());
4277 prefs.setDelayEnabledTransitionDelayMode(DelayEnabledTransitionControl.getDefaultDelayMode());
4278 prefs.setDelayEnabledTransitionGranularity(DelayEnabledTransitionControl.getDefaultGranularity());
4279 prefs.setDelayEnabledTransitionIsRandomTransition(DelayEnabledTransitionControl.isRandomTransition());
4280@@ -900,20 +1046,27 @@
4281 "Workspace Saved", JOptionPane.INFORMATION_MESSAGE);
4282 }
4283
4284+
4285 private void buildToolbar() {
4286+
4287+ //XXX .setRequestFocusEnabled(false), removed "border" around tollbar buttons when selcted/focus
4288+ // https://stackoverflow.com/questions/9361658/disable-jbutton-focus-border and
4289+ //https://stackoverflow.com/questions/20169436/how-to-prevent-toolbar-button-focus-in-java-swing
4290+
4291 // Create the toolbar
4292 JToolBar toolBar = new JToolBar();
4293 toolBar.setFloatable(false);// Inhibit toolbar floating
4294+ toolBar.setRequestFocusEnabled(false);
4295
4296 // Basis file operations
4297- toolBar.add(createAction);
4298- toolBar.add(openAction);
4299- toolBar.add(saveAction);
4300- toolBar.add(saveAsAction);
4301+ toolBar.add(createAction).setRequestFocusEnabled(false);
4302+ toolBar.add(openAction).setRequestFocusEnabled(false);
4303+ toolBar.add(saveAction).setRequestFocusEnabled(false);
4304+ toolBar.add(saveAsAction).setRequestFocusEnabled(false);
4305
4306 // Print
4307 toolBar.addSeparator();
4308- toolBar.add(printAction);
4309+ toolBar.add(printAction).setRequestFocusEnabled(false);
4310
4311 // Copy/past
4312 /*
4313@@ -924,32 +1077,46 @@
4314
4315 // Undo/redo
4316 toolBar.addSeparator();
4317- toolBar.add(deleteAction);
4318- toolBar.add(undoAction);
4319- toolBar.add(redoAction);
4320+ toolBar.add(deleteAction).setRequestFocusEnabled(false);
4321+ toolBar.add(undoAction).setRequestFocusEnabled(false);
4322+ toolBar.add(redoAction).setRequestFocusEnabled(false);
4323
4324 // Zoom
4325 toolBar.addSeparator();
4326- toolBar.add(zoomOutAction);
4327- addZoomComboBox(toolBar, new ZoomAction("Zoom",
4328- "Select zoom percentage ", ""));
4329- toolBar.add(zoomInAction);
4330+ toolBar.add(zoomOutAction).setRequestFocusEnabled(false);
4331+ addZoomComboBox(toolBar, new GuiAction("Zoom", "Select zoom percentage ", "") {
4332+ @Override
4333+ public void actionPerformed(ActionEvent e) {
4334+ String selectedZoomLevel = (String) zoomComboBox.getSelectedItem();
4335+ //parse selected zoom level, and strip of %.
4336+ int newZoomLevel = Integer.parseInt(selectedZoomLevel.replace("%", ""));
4337+
4338+ boolean didZoom = appView.getZoomController().setZoom(newZoomLevel);
4339+ if (didZoom) {
4340+ updateZoomCombo();
4341+ appView.zoomToMidPoint(); //Do Zoom
4342+ }
4343+ }
4344+ });
4345+ toolBar.add(zoomInAction).setRequestFocusEnabled(false);
4346
4347 // Modes
4348
4349 toolBar.addSeparator();
4350- toolBar.add(toggleGrid);
4351+ toolBar.add(toggleGrid).setRequestFocusEnabled(false);
4352+
4353 toolBar.add(new ToggleButton(startAction));
4354
4355 // Start drawingToolBar
4356 drawingToolBar = new JToolBar();
4357 drawingToolBar.setFloatable(false);
4358 drawingToolBar.addSeparator();
4359+ drawingToolBar.setRequestFocusEnabled(false);
4360
4361 // Normal arraw
4362-
4363 drawingToolBar.add(new ToggleButton(selectAction));
4364
4365+
4366 // Drawing elements
4367 drawingToolBar.addSeparator();
4368 drawingToolBar.add(new ToggleButton(timedPlaceAction));
4369@@ -967,7 +1134,7 @@
4370
4371 // Create panel to put toolbars in
4372 JPanel toolBarPanel = new JPanel();
4373- toolBarPanel.setLayout(new FlowLayout(0, 0, 0));
4374+ toolBarPanel.setLayout(new FlowLayout(FlowLayout.LEFT, 0, 0));
4375
4376 // Add toolbars to pane
4377 toolBarPanel.add(toolBar);
4378@@ -990,17 +1157,30 @@
4379 /**
4380 * @author Ben Kirby Takes the method of setting up the Zoom menu out of the
4381 * main buildMenus method.
4382- * @param JMenu
4383+ * @param zoomMenu
4384 * - the menu to add the submenu to
4385 */
4386 private void addZoomMenuItems(JMenu zoomMenu) {
4387 for (int i = 0; i <= zoomExamples.length - 1; i++) {
4388- ZoomAction a = new ZoomAction(zoomExamples[i], "Select zoom percentage", "");
4389-
4390- JMenuItem newItem = new JMenuItem(a);
4391-
4392- zoomMenu.add(newItem);
4393+
4394+ final int zoomper = zoomExamples[i];
4395+ GuiAction newZoomAction = new GuiAction(zoomExamples[i] + "%", "Select zoom percentage", "") {
4396+ @Override
4397+ public void actionPerformed(ActionEvent e) {
4398+ boolean didZoom = appView.getZoomController().setZoom(zoomper);
4399+ if (didZoom) {
4400+ updateZoomCombo();
4401+ appView.zoomToMidPoint(); //Do Zoom
4402+ }
4403+ }
4404+ };
4405+
4406+ //JMenuItem newItem = new JMenuItem(a);
4407+
4408+ zoomMenu.add(newZoomAction);
4409 }
4410+
4411+
4412 }
4413
4414 /**
4415@@ -1014,7 +1194,14 @@
4416 */
4417 private void addZoomComboBox(JToolBar toolBar, Action action) {
4418 Dimension zoomComboBoxDimension = new Dimension(75, 28);
4419- zoomComboBox = new JComboBox(zoomExamples);
4420+
4421+ String[] zoomExamplesStrings = new String[zoomExamples.length];
4422+ int i;
4423+ for (i=0; i < zoomExamples.length; i++) {
4424+ zoomExamplesStrings[i] = zoomExamples[i] + "%";
4425+ }
4426+
4427+ zoomComboBox = new JComboBox<String>(zoomExamplesStrings);
4428 zoomComboBox.setEditable(true);
4429 zoomComboBox.setSelectedItem("100%");
4430 zoomComboBox.setMaximumRowCount(zoomExamples.length);
4431@@ -1026,21 +1213,10 @@
4432 toolBar.add(zoomComboBox);
4433 }
4434
4435- private JMenuItem addMenuItem(JMenu menu, Action action) {
4436- JMenuItem item = menu.add(action);
4437- KeyStroke keystroke = (KeyStroke) action.getValue(Action.ACCELERATOR_KEY);
4438-
4439- if (keystroke != null) {
4440- item.setAccelerator(keystroke);
4441- }
4442- return item;
4443- }
4444-
4445- private JMenuItem addCheckboxMenuItem(JMenu menu, boolean selected, Action action) {
4446- return addCheckboxMenuItem(menu, selected, action, new JCheckBoxMenuItem());
4447- }
4448-
4449- private JMenuItem addCheckboxMenuItem(JMenu menu, boolean selected, Action action, JCheckBoxMenuItem checkBoxItem) {
4450+ private JCheckBoxMenuItem addCheckboxMenuItem(JMenu menu, boolean selected, Action action) {
4451+
4452+ JCheckBoxMenuItem checkBoxItem = new JCheckBoxMenuItem();
4453+
4454 checkBoxItem.setAction(action);
4455 checkBoxItem.setSelected(selected);
4456 JMenuItem item = menu.add(checkBoxItem);
4457@@ -1049,7 +1225,7 @@
4458 if (keystroke != null) {
4459 item.setAccelerator(keystroke);
4460 }
4461- return item;
4462+ return checkBoxItem;
4463 }
4464
4465 /**
4466@@ -1150,17 +1326,17 @@
4467 // Remove constant highlight
4468 CreateGui.getCurrentTab().removeConstantHighlights();
4469
4470- CreateGui.getAnimationController().requestFocusInWindow();
4471+ CreateGui.getCurrentTab().getAnimationController().requestFocusInWindow();
4472
4473 // Event repeater
4474- ((JPanel) CreateGui.getAnimationController()).getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_RIGHT, 0, false), "_right_hold");
4475- ((JPanel) CreateGui.getAnimationController()).getActionMap().put("_right_hold", stepforwardAction);
4476- ((JPanel) CreateGui.getAnimationController()).getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_LEFT, 0, false), "_left_hold");
4477- ((JPanel) CreateGui.getAnimationController()).getActionMap().put("_left_hold", stepbackwardAction);
4478- ((JPanel) CreateGui.getAnimationController()).getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_UP, 0, false), "_up_hold");
4479- ((JPanel) CreateGui.getAnimationController()).getActionMap().put("_up_hold", prevcomponentAction);
4480- ((JPanel) CreateGui.getAnimationController()).getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_DOWN, 0, false), "_down_hold");
4481- ((JPanel) CreateGui.getAnimationController()).getActionMap().put("_down_hold", nextcomponentAction);
4482+ CreateGui.getCurrentTab().getAnimationController().getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_RIGHT, 0, false), "_right_hold");
4483+ CreateGui.getCurrentTab().getAnimationController().getActionMap().put("_right_hold", stepforwardAction);
4484+ CreateGui.getCurrentTab().getAnimationController().getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_LEFT, 0, false), "_left_hold");
4485+ CreateGui.getCurrentTab().getAnimationController().getActionMap().put("_left_hold", stepbackwardAction);
4486+ CreateGui.getCurrentTab().getAnimationController().getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_UP, 0, false), "_up_hold");
4487+ CreateGui.getCurrentTab().getAnimationController().getActionMap().put("_up_hold", prevcomponentAction);
4488+ CreateGui.getCurrentTab().getAnimationController().getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_DOWN, 0, false), "_down_hold");
4489+ CreateGui.getCurrentTab().getAnimationController().getActionMap().put("_down_hold", nextcomponentAction);
4490 break;
4491 case noNet:
4492 exportTraceAction.setEnabled(false);
4493@@ -1249,7 +1425,7 @@
4494 startAction.setEnabled(enable);
4495
4496 // Tools
4497- statistics.setEnabled(enable);
4498+ netStatisticsAction.setEnabled(enable);
4499
4500 }
4501
4502@@ -1258,42 +1434,59 @@
4503 appView = CreateGui.getDrawingSurface(index);
4504 }
4505
4506+ //XXX 2018-05-23 kyrke, implementation close to closeTab, needs refactoring
4507+ private void undoAddTab(int currentlySelected) {
4508+ CreateGui.removeTab(appTab.getSelectedIndex() );
4509+ appTab.removeTabAt(appTab.getSelectedIndex());
4510+ appTab.setSelectedIndex(currentlySelected);
4511+ //Update DrawingSurfaceImpl manually. Bug #1543124
4512+ setObjects(appTab.getSelectedIndex());
4513+ }
4514+
4515 // set tabbed pane properties and add change listener that updates tab with
4516 // linked model and view
4517- public void setTab() {
4518+ public void setChangeListenerOnTab() {
4519
4520- appTab = CreateGui.getTab();
4521 appTab.addChangeListener(new ChangeListener() {
4522
4523 public void stateChanged(ChangeEvent e) {
4524
4525 int index = appTab.getSelectedIndex();
4526- setObjects(index);
4527- if (appView != null) {
4528- appView.setVisible(true);
4529- appView.repaint();
4530- updateZoomCombo();
4531-
4532- setTitle(appTab.getTitleAt(index));
4533- setGUIMode(GUIMode.draw);
4534-
4535- // TODO: change this code... it's ugly :)
4536- if (appGui.getMode() == ElementType.SELECT) {
4537- appGui.activateSelectAction();
4538- }
4539-
4540- } else {
4541- setTitle(null);
4542- }
4543+ changeToTab(index);
4544
4545 }
4546
4547 });
4548- appGui = CreateGui.getApp();
4549- appView = CreateGui.getView();
4550-
4551- }
4552-
4553+ }
4554+
4555+ //TODO: 2018-05-07 //kyrke Create CloseTab function, used to close a tab
4556+ //TODO: Refactor the setObject (bad name), inline in changeToTab/Close Tab and use changeToTab in newTab
4557+
4558+ private void changeToTab(int index) {
4559+
4560+ //If tab is changed by something else that by clicking a tab then change to the tab.
4561+ if (appTab.getSelectedIndex() != index) {
4562+ appTab.setSelectedIndex(index);
4563+ }
4564+
4565+ setObjects(index);
4566+ if (appView != null) {
4567+ appView.setVisible(true);
4568+ appView.repaint();
4569+ updateZoomCombo();
4570+
4571+ setTitle(appTab.getTitleAt(index));
4572+ setGUIMode(GUIMode.draw);
4573+
4574+ // TODO: change this code... it's ugly :)
4575+ if (getMode() == ElementType.SELECT) {
4576+ activateSelectAction();
4577+ }
4578+
4579+ } else {
4580+ setTitle(null);
4581+ }
4582+ }
4583
4584
4585 // HAK Method called by netModel object when it changes
4586@@ -1303,98 +1496,97 @@
4587 }
4588 }
4589
4590- public void showQueries(boolean enable){
4591+ private void showQueries(boolean enable){
4592 showQueries = enable;
4593 CreateGui.getCurrentTab().showQueries(enable);
4594- showQueriesCheckBox.setSelected(enable);
4595+
4596 }
4597- public void toggleQueries(){
4598+ private void toggleQueries(){
4599 showQueries(!showQueries);
4600 }
4601
4602- public void showConstants(boolean enable){
4603+ private void showConstants(boolean enable){
4604 showConstants = enable;
4605 CreateGui.getCurrentTab().showConstantsPanel(enable);
4606- showConstantsCheckBox.setSelected(enable);
4607+
4608 }
4609- public void toggleConstants(){
4610+ private void toggleConstants(){
4611 showConstants(!showConstants);
4612 }
4613
4614- public void showToolTips(boolean enable){
4615+ private void showToolTips(boolean enable){
4616 showToolTips = enable;
4617 Preferences.getInstance().setShowToolTips(showToolTips);
4618- showToolTipsCheckBox.setSelected(enable);
4619+
4620 ToolTipManager.sharedInstance().setEnabled(enable);
4621 ToolTipManager.sharedInstance().setInitialDelay(400);
4622 ToolTipManager.sharedInstance().setReshowDelay(800);
4623 ToolTipManager.sharedInstance().setDismissDelay(60000);
4624 }
4625- public void toggleToolTips(){
4626+ private void toggleToolTips(){
4627 showToolTips(!showToolTips);
4628 }
4629
4630- public boolean isShowingToolTips(){
4631+ boolean isShowingToolTips(){
4632 return showToolTips;
4633 }
4634
4635- public void toggleTokenAge(){
4636- CreateGui.toggleShowTokenAge();
4637- Preferences.getInstance().setShowTokenAge(CreateGui.showTokenAge());
4638- appView.repaintAll();
4639- }
4640-
4641- public void toggleZeroToInfinityIntervals() {
4642- CreateGui.toggleShowZeroToInfinityIntervals();
4643- Preferences.getInstance().setShowZeroInfIntervals(CreateGui.showZeroToInfinityIntervals());
4644- appView.repaintAll();
4645- }
4646-
4647- public void showComponents(boolean enable){
4648+ private void toggleTokenAge(){
4649+ toggleShowTokenAge();
4650+ Preferences.getInstance().setShowTokenAge(showTokenAge());
4651+ appView.repaintAll();
4652+ }
4653+
4654+ private void toggleZeroToInfinityIntervals() {
4655+ toggleShowZeroToInfinityIntervals();
4656+ Preferences.getInstance().setShowZeroInfIntervals(showZeroToInfinityIntervals());
4657+ appView.repaintAll();
4658+ }
4659+
4660+ private void showComponents(boolean enable){
4661 showComponents = enable;
4662 CreateGui.getCurrentTab().showComponents(enable);
4663- showComponentsCheckBox.setSelected(enable);
4664+
4665 }
4666- public void toggleComponents(){
4667+ private void toggleComponents(){
4668 showComponents(!showComponents);
4669 }
4670
4671- public void showEnabledTransitionsList(boolean enable){
4672+ private void showEnabledTransitionsList(boolean enable){
4673 showEnabledTransitions = enable;
4674 CreateGui.getCurrentTab().showEnabledTransitionsList(enable);
4675- showEnabledTransitionsCheckBox.setSelected(enable);
4676+
4677 }
4678- public void toggleEnabledTransitionsList(){
4679+ private void toggleEnabledTransitionsList(){
4680 showEnabledTransitionsList(!showEnabledTransitions);
4681 }
4682
4683- public void showDelayEnabledTransitions(boolean enable){
4684+ private void showDelayEnabledTransitions(boolean enable){
4685 showDelayEnabledTransitions = enable;
4686 CreateGui.getCurrentTab().showDelayEnabledTransitions(enable);
4687- showDelayEnabledTransitionsCheckBox.setSelected(enable);
4688 }
4689- public void toggleDelayEnabledTransitions(){
4690+ private void toggleDelayEnabledTransitions(){
4691 showDelayEnabledTransitions(!showDelayEnabledTransitions);
4692 }
4693
4694- public void saveOperation(boolean forceSave){
4695+ private void saveOperation(boolean forceSave){
4696 saveOperation(appTab.getSelectedIndex(), forceSave);
4697 }
4698
4699- public boolean saveOperation(int index, boolean forceSaveAs) {
4700- File modelFile = CreateGui.getFile(index);
4701- boolean result = false;
4702+ private boolean saveOperation(int index, boolean forceSaveAs) {
4703+ File modelFile = CreateGui.getTab(index).getFile();
4704+ boolean result;
4705 if (!forceSaveAs && modelFile != null) { // ordinary save
4706 saveNet(index, modelFile);
4707 result = true;
4708 } else { // save as
4709- String path = null;
4710+ String path;
4711 if (modelFile != null) {
4712 path = modelFile.toString();
4713 } else {
4714 path = appTab.getTitleAt(index);
4715 }
4716- String filename = new FileBrowser(path).saveFile();
4717+ String filename = FileBrowser.constructor("Timed-Arc Petri Net", "xml", path).saveFile();
4718 if (filename != null) {
4719 modelFile = new File(filename);
4720 saveNet(index, modelFile);
4721@@ -1414,7 +1606,7 @@
4722 try {
4723 saveNet(index, outFile, (List<TAPNQuery>) CreateGui.getTab(index).queries());
4724
4725- CreateGui.setFile(outFile, index);
4726+ CreateGui.getCurrentTab().setFile(outFile);
4727
4728 CreateGui.getDrawingSurface(index).setNetChanged(false);
4729 appTab.setTitleAt(index, outFile.getName());
4730@@ -1436,7 +1628,7 @@
4731 NetworkMarking currentMarking = null;
4732 if(getGUIMode().equals(GUIMode.animation)){
4733 currentMarking = currentTab.network().marking();
4734- currentTab.network().setMarking(CreateGui.getAnimator().getInitialMarking());
4735+ currentTab.network().setMarking(getAnimator().getInitialMarking());
4736 }
4737
4738 NetWriter tapnWriter = new TimedArcPetriNetNetworkWriter(
4739@@ -1452,62 +1644,64 @@
4740 currentTab.network().setMarking(currentMarking);
4741 }
4742 } catch (Exception e) {
4743- System.err.println(e);
4744+ Logger.log(e);
4745 JOptionPane.showMessageDialog(GuiFrame.this, e.toString(),
4746 "File Output Error", JOptionPane.ERROR_MESSAGE);
4747- return;
4748 }
4749 }
4750
4751- public void createNewTab(String name, NetType netType) {
4752- int freeSpace = CreateGui.getFreeSpace(netType);
4753-
4754- setObjects(freeSpace);
4755- CreateGui.getModel(freeSpace).setNetType(netType);
4756+
4757+ public void createNewEmptyTab(String name, NetType netType){
4758+ TabContent tab = new TabContent(NetType.TAPN);
4759+
4760+ //Set Default Template
4761+ String templateName = tab.drawingSurface().getNameGenerator().getNewTemplateName();
4762+ Template template = new Template(new TimedArcPetriNet(templateName), new DataLayer(), new Zoomer());
4763+ tab.addTemplate(template, false);
4764+
4765+ createNewTab(name, tab);
4766+ }
4767+
4768+ public void createNewTab(String name, TabContent tab) {
4769+ //int freeSpace = CreateGui.getFreeSpace(netType);
4770+
4771+ //setObjects(freeSpace);
4772+ //CreateGui.getModel(freeSpace).setNetType(netType);
4773
4774 if (name == null || name.isEmpty()) {
4775 name = "New Petri net " + (newNameCounter++) + ".xml";
4776 }
4777-
4778- TabContent tab = CreateGui.getTab(freeSpace);
4779+
4780+ //tab.setCurrentTemplate(template);
4781+ CreateGui.addTab(tab);
4782 appTab.addTab(name, tab);
4783- appTab.setTabComponentAt(freeSpace, new TabComponent(appTab));
4784- appTab.setSelectedIndex(freeSpace);
4785-
4786- String templateName = tab.drawingSurface().getNameGenerator().getNewTemplateName();
4787- Template template = new Template(new TimedArcPetriNet(templateName), new DataLayer(), new Zoomer());
4788- tab.addTemplate(template);
4789-
4790- tab.setCurrentTemplate(template);
4791-
4792- appView.setNetChanged(false); // Status is unchanged
4793- appView.updatePreferredSize();
4794-
4795- setTitle(name);// Change the program caption
4796- appTab.setTitleAt(freeSpace, name);
4797- selectAction.actionPerformed(null);
4798+ int newTabIndex = appTab.getTabCount()-1;
4799+ appTab.setTabComponentAt(newTabIndex, new TabComponent(appTab));
4800+
4801+ //appView.setNetChanged(false); // Status is unchanged
4802+ //appView.updatePreferredSize();
4803+
4804+ //setTitle(name);// Change the program caption
4805+ //appTab.setTitleAt(freeSpace, name);
4806+ //selectAction.actionPerformed(null);
4807+ changeToTab(newTabIndex);
4808 }
4809
4810
4811 /**
4812 * Creates a new tab with the selected file, or a new file if filename==null
4813- *
4814- * @param filename
4815- * Filename of net to load, or <b>null</b> to create a new, empty
4816- * tab
4817 */
4818- public void createNewTabFromFile(InputStream file, String namePrefix) {
4819+ public TabContent createNewTabFromFile(InputStream file, String name) {
4820 int freeSpace = CreateGui.getFreeSpace(NetType.TAPN);
4821- String name = "";
4822+
4823
4824 setObjects(freeSpace);
4825 int currentlySelected = appTab.getSelectedIndex();
4826
4827-
4828- if (namePrefix == null || namePrefix.equals("")) {
4829+ if (name == null || name.equals("")) {
4830 name = "New Petri net " + (newNameCounter++) + ".xml";
4831- } else {
4832- name = namePrefix + ".xml";
4833+ } else if (!name.toLowerCase().endsWith(".xml")){
4834+ name = name + ".xml";
4835 }
4836
4837 TabContent tab = CreateGui.getTab(freeSpace);
4838@@ -1515,56 +1709,52 @@
4839 appTab.setTabComponentAt(freeSpace, new TabComponent(appTab));
4840 appTab.setSelectedIndex(freeSpace);
4841
4842- if (file != null) {
4843- try {
4844- TabContent currentTab = (TabContent) appTab.getSelectedComponent();
4845- if (CreateGui.getApp() != null) {
4846- // Notifies used to indicate new instances.
4847- CreateGui.getApp().setMode(ElementType.CREATING);
4848- }
4849-
4850- ModelLoader loader = new ModelLoader(currentTab.drawingSurface());
4851- LoadedModel loadedModel = loader.load(file);
4852-
4853- currentTab.setNetwork(loadedModel.network(), loadedModel.templates());
4854- currentTab.setQueries(loadedModel.queries());
4855- currentTab.setConstants(loadedModel.network().constants());
4856- currentTab.setupNameGeneratorsFromTemplates(loadedModel.templates());
4857-
4858- currentTab.selectFirstElements();
4859-
4860- if (CreateGui.getApp() != null) {
4861- CreateGui.getApp().restoreMode();
4862- }
4863-
4864- CreateGui.setFile(null, freeSpace);
4865- } catch (Exception e) {
4866- undoAddTab(currentlySelected);
4867- JOptionPane.showMessageDialog(GuiFrame.this,
4868- "TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString(),
4869- "Error loading file: " + name,
4870- JOptionPane.ERROR_MESSAGE);
4871- return;
4872- }
4873+
4874+ try {
4875+ if (CreateGui.getApp() != null) {
4876+ // Notifies used to indicate new instances.
4877+ CreateGui.getApp().setMode(ElementType.CREATING);
4878+ }
4879+
4880+ ModelLoader loader = new ModelLoader(tab.drawingSurface());
4881+ LoadedModel loadedModel = loader.load(file);
4882+
4883+ tab.setNetwork(loadedModel.network(), loadedModel.templates());
4884+ tab.setQueries(loadedModel.queries());
4885+ tab.setConstants(loadedModel.network().constants());
4886+ tab.setupNameGeneratorsFromTemplates(loadedModel.templates());
4887+
4888+ tab.selectFirstElements();
4889+
4890+ if (CreateGui.getApp() != null) {
4891+ CreateGui.getApp().restoreMode();
4892+ }
4893+
4894+ tab.setFile(null);
4895+ } catch (Exception e) {
4896+ undoAddTab(currentlySelected);
4897+ JOptionPane.showMessageDialog(GuiFrame.this,
4898+ "TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString(),
4899+ "Error loading file: " + name,
4900+ JOptionPane.ERROR_MESSAGE);
4901+ return null;
4902 }
4903
4904- appView.setNetChanged(false); // Status is unchanged
4905- appView.updatePreferredSize();
4906+
4907+ //appView.updatePreferredSize(); //XXX 2018-05-23 kyrke seems not to be needed
4908 setTitle(name);// Change the program caption
4909- appTab.setTitleAt(freeSpace, name);
4910+ //appTab.setTitleAt(freeSpace, name); //Set above in addTab
4911 selectAction.actionPerformed(null);
4912+ return tab;
4913 }
4914
4915+
4916 /**
4917 * Creates a new tab with the selected file, or a new file if filename==null
4918- *
4919- * @param filename
4920- * Filename of net to load, or <b>null</b> to create a new, empty
4921- * tab
4922 */
4923- public void createNewTabFromFile(File file, boolean loadPNML) {
4924+ public void createNewTabFromPNMLFile(File file) {
4925 int freeSpace = CreateGui.getFreeSpace(NetType.TAPN);
4926- String name = "";
4927+ String name;
4928
4929 setObjects(freeSpace);
4930 int currentlySelected = appTab.getSelectedIndex();
4931@@ -1582,53 +1772,62 @@
4932
4933 if (file != null) {
4934 try {
4935- TabContent currentTab = (TabContent) appTab.getSelectedComponent();
4936 if (CreateGui.getApp() != null) {
4937 // Notifies used to indicate new instances.
4938 CreateGui.getApp().setMode(ElementType.CREATING);
4939 }
4940
4941 LoadedModel loadedModel;
4942- if(loadPNML){
4943- PNMLoader loader = new PNMLoader(currentTab.drawingSurface());
4944- loadedModel = loader.load(file);
4945- } else {
4946- ModelLoader loader = new ModelLoader(currentTab.drawingSurface());
4947- loadedModel = loader.load(file);
4948- }
4949-
4950- currentTab.setNetwork(loadedModel.network(), loadedModel.templates());
4951- currentTab.setQueries(loadedModel.queries());
4952- currentTab.setConstants(loadedModel.network().constants());
4953- currentTab.setupNameGeneratorsFromTemplates(loadedModel.templates());
4954-
4955- currentTab.selectFirstElements();
4956+
4957+ PNMLoader loader = new PNMLoader(tab.drawingSurface());
4958+ loadedModel = loader.load(file);
4959+
4960+
4961+ tab.setNetwork(loadedModel.network(), loadedModel.templates());
4962+ tab.setQueries(loadedModel.queries());
4963+ tab.setConstants(loadedModel.network().constants());
4964+ tab.setupNameGeneratorsFromTemplates(loadedModel.templates());
4965+
4966+ tab.selectFirstElements();
4967
4968 if (CreateGui.getApp() != null) {
4969 CreateGui.getApp().restoreMode();
4970 }
4971
4972- if(!loadPNML){
4973- CreateGui.setFile(file, freeSpace);
4974- }
4975 } catch (Exception e) {
4976 undoAddTab(currentlySelected);
4977 JOptionPane.showMessageDialog(GuiFrame.this,
4978- "TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString(),
4979- "Error loading file: " + name,
4980+ "TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString(),
4981+ "Error loading file: " + name,
4982 JOptionPane.ERROR_MESSAGE);
4983 return;
4984 }
4985 }
4986
4987- appView.setNetChanged(false); // Status is unchanged
4988- appView.updatePreferredSize();
4989- name = name.replace(".pnml",".xml"); // rename .pnml input file to .xml
4990+ //appView.updatePreferredSize(); //XXX 2018-05-23 kyrke seems not to be needed
4991+ name = name.replace(".pnml",".xml"); // rename .pnml input file to .xml
4992 setTitle(name);// Change the program caption
4993- appTab.setTitleAt(freeSpace, name);
4994+ //appTab.setTitleAt(freeSpace, name); //Set above in addTab
4995 selectAction.actionPerformed(null);
4996 }
4997
4998+
4999+ /**
5000+ * Creates a new tab with the selected file, or a new file if filename==null
The diff has been truncated for viewing.

Subscribers

People subscribed via source and target branches