Merge lp:~yrke/tapaal/guirefactor into lp:tapaal
- guirefactor
- Merge into trunk
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 | ||||||||||||||||
Related bugs: |
|
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.
Description of the change
Kenneth Yrke Jørgensen (yrke) wrote : | # |
- 1137. By Kenneth Yrke Jørgensen
-
Merged branch, Implements zoome using scrollwheel with ctrl
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/
InputStream file = Thread.
src/pipe/
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
- 1138. By Kenneth Yrke Jørgensen
-
fixed closure to use final variable to allow to compile to java 1.6
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.
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.
Kenneth Yrke Jørgensen (yrke) wrote : | # |
Hmm... shortcuts has been overwritten ala:
saveAction.
instead of setting them in the correct way, should be a relative simple fix.
- 1139. By Kenneth Yrke Jørgensen
-
Fixed some actions using hardcoded ctrl as shortcutkey
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.
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).
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?
Jiri Srba (srba) wrote : | # |
Tested on mac and all seems to work fine, so I am going to merge it to trunk.
Preview Diff
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 | |
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 |
Please test loading of PNML files