← Back to branch summary

~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/pipe/gui/widgets/TAPNTransitionEditor.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-04-12 09:50:16 UTC
  • mfrom: (329.1.188 tapaal-1.5)
  • Revision ID: mail@yrke.dk-20110412095016-e4hqdgab5596ja09
Merged with branch addning support for new 1.5 features

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/TAPNTransitionEditor.java
1
1
package pipe.gui.widgets;
2
2
 
3
3
import java.awt.Color;
4
 
import java.util.regex.Pattern;
 
4
import java.awt.Dimension;
 
5
import java.awt.GridBagConstraints;
 
6
import java.awt.event.ActionEvent;
 
7
import java.awt.event.ActionListener;
5
8
 
 
9
import javax.swing.JCheckBox;
 
10
import javax.swing.JComboBox;
6
11
import javax.swing.JOptionPane;
7
12
import javax.swing.JRootPane;
8
13
import javax.swing.JTextField;
9
14
import javax.swing.event.CaretListener;
10
15
 
11
 
import pipe.dataLayer.DataLayer;
12
 
import pipe.dataLayer.Transition;
13
 
import pipe.gui.CreateGui;
14
 
import pipe.gui.GuiView;
15
 
 
16
 
 
17
 
/**
18
 
 *
19
 
 * @author Kenneth and Joakim on a base made by pere
20
 
 */
21
 
public class TAPNTransitionEditor 
22
 
extends javax.swing.JPanel {
23
 
 
24
 
        /**
25
 
         * 
26
 
         */
 
16
import pipe.dataLayer.TimedTransitionComponent;
 
17
import dk.aau.cs.gui.Context;
 
18
import dk.aau.cs.gui.undo.MakeTransitionSharedCommand;
 
19
import dk.aau.cs.gui.undo.RenameTimedTransitionCommand;
 
20
import dk.aau.cs.gui.undo.UnshareTransitionCommand;
 
21
import dk.aau.cs.model.tapn.SharedTransition;
 
22
import dk.aau.cs.model.tapn.TimedInhibitorArc;
 
23
import dk.aau.cs.model.tapn.TimedInputArc;
 
24
import dk.aau.cs.model.tapn.TimedOutputArc;
 
25
import dk.aau.cs.model.tapn.TimedTransition;
 
26
import dk.aau.cs.model.tapn.TransportArc;
 
27
import dk.aau.cs.util.RequireException;
 
28
 
 
29
public class TAPNTransitionEditor extends javax.swing.JPanel {
27
30
        private static final long serialVersionUID = 1744651413834659994L;
28
 
        Transition transition;
29
 
        boolean attributesVisible;
30
 
        boolean timed;
31
 
        boolean infiniteServer;
32
 
        Integer priority = 0;
33
 
        String name;   
34
 
        DataLayer pnmlData;
35
 
        GuiView view;
36
 
        JRootPane rootPane;
 
31
        private TimedTransitionComponent transition;
 
32
        private JRootPane rootPane;
 
33
        private Context context;
37
34
 
38
 
        /**
39
 
         * Creates new form TransitionEditor
40
 
         */
41
 
        public TAPNTransitionEditor(JRootPane _rootPane, Transition _transition, 
42
 
                        DataLayer _pnmlData, GuiView _view) {
 
35
        public TAPNTransitionEditor(JRootPane _rootPane, TimedTransitionComponent _transition, Context context) {
43
36
                rootPane = _rootPane;
44
37
                transition = _transition;
45
 
                pnmlData = _pnmlData;
46
 
                view = _view;
47
 
                name = transition.getName();
48
 
                timed = transition.isTimed();
49
 
                infiniteServer = transition.isInfiniteServer();
50
 
 
 
38
                this.context = context;
51
39
                initComponents();
52
40
 
53
41
                rootPane.setDefaultButton(okButton);
54
 
 
55
 
                attributesVisible = transition.getAttributesVisible();
56
42
        }
57
43
 
58
 
        /** This method is called from within the constructor to
59
 
         * initialize the form.
60
 
         * WARNING: Do NOT modify this code. The content of this method is
61
 
         * always regenerated by the Form Editor.
62
 
         */
63
 
        // <editor-fold defaultstate="collapsed" desc=" Generated Code ">//GEN-BEGIN:initComponents
64
44
        private void initComponents() {
65
45
                java.awt.GridBagConstraints gridBagConstraints;
66
46
 
67
47
                transitionEditorPanel = new javax.swing.JPanel();
68
48
                nameLabel = new javax.swing.JLabel();
69
49
                nameTextField = new javax.swing.JTextField();
 
50
                nameTextField.setPreferredSize(new Dimension(120,27));
70
51
                rotationLabel = new javax.swing.JLabel();
71
52
                rotationComboBox = new javax.swing.JComboBox();
72
53
                buttonPanel = new javax.swing.JPanel();
73
54
                cancelButton = new javax.swing.JButton();
74
55
                okButton = new javax.swing.JButton();
75
 
 
 
56
                sharedCheckBox = new JCheckBox("Shared");
 
57
                sharedTransitionsComboBox = new JComboBox(context.network().sharedTransitions().toArray());
 
58
                sharedTransitionsComboBox.setPreferredSize(new Dimension(120,27));
76
59
                setLayout(new java.awt.GridBagLayout());
77
60
 
78
61
                transitionEditorPanel.setLayout(new java.awt.GridBagLayout());
79
 
 
80
62
                transitionEditorPanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Transition Editor"));
 
63
 
 
64
                sharedCheckBox.addActionListener(new ActionListener(){
 
65
                        public void actionPerformed(ActionEvent arg0) {
 
66
                                JCheckBox box = (JCheckBox)arg0.getSource();
 
67
                                if(box.isSelected()){
 
68
                                        switchToNameDropDown();
 
69
                                }else{
 
70
                                        switchToNameTextField();
 
71
                                }
 
72
                        }               
 
73
                });
 
74
                sharedCheckBox.setEnabled(context.network().numberOfSharedTransitions() > 0 && !hasArcsToSharedPlaces(transition.underlyingTransition()));
 
75
                gridBagConstraints = new java.awt.GridBagConstraints();
 
76
                gridBagConstraints.gridx = 1;
 
77
                gridBagConstraints.gridy = 0;
 
78
                gridBagConstraints.anchor = java.awt.GridBagConstraints.WEST;
 
79
                gridBagConstraints.insets = new java.awt.Insets(3, 3, 3, 3);
 
80
                transitionEditorPanel.add(sharedCheckBox, gridBagConstraints);
 
81
 
81
82
                nameLabel.setText("Name:");
82
83
                gridBagConstraints = new java.awt.GridBagConstraints();
83
84
                gridBagConstraints.gridx = 0;
84
 
                gridBagConstraints.gridy = 0;
 
85
                gridBagConstraints.gridy = 1;
85
86
                gridBagConstraints.anchor = java.awt.GridBagConstraints.EAST;
86
87
                gridBagConstraints.insets = new java.awt.Insets(3, 3, 3, 3);
87
88
                transitionEditorPanel.add(nameLabel, gridBagConstraints);
88
89
 
89
 
                nameTextField.setText(transition.getName());
90
90
                nameTextField.addFocusListener(new java.awt.event.FocusAdapter() {
91
91
                        @Override
92
92
                        public void focusGained(java.awt.event.FocusEvent evt) {
93
93
                                nameTextFieldFocusGained(evt);
94
94
                        }
 
95
 
95
96
                        @Override
96
97
                        public void focusLost(java.awt.event.FocusEvent evt) {
97
98
                                nameTextFieldFocusLost(evt);
98
99
                        }
99
100
                });
100
101
 
101
 
                gridBagConstraints = new java.awt.GridBagConstraints();
102
 
                gridBagConstraints.gridx = 1;
103
 
                gridBagConstraints.gridy = 0;
104
 
                gridBagConstraints.gridwidth = 3;
105
 
                gridBagConstraints.fill = java.awt.GridBagConstraints.HORIZONTAL;
106
 
                gridBagConstraints.insets = new java.awt.Insets(3, 3, 3, 3);
107
 
                transitionEditorPanel.add(nameTextField, gridBagConstraints);
108
 
 
109
102
                rotationLabel.setText("Rotate:");
110
103
                gridBagConstraints = new java.awt.GridBagConstraints();
111
104
                gridBagConstraints.gridx = 0;
112
 
                gridBagConstraints.gridy = 5;
 
105
                gridBagConstraints.gridy = 2;
113
106
                gridBagConstraints.anchor = java.awt.GridBagConstraints.NORTH;
114
107
                gridBagConstraints.insets = new java.awt.Insets(3, 3, 3, 3);
115
108
                transitionEditorPanel.add(rotationLabel, gridBagConstraints);
116
109
 
117
 
                rotationComboBox.setModel(new javax.swing.DefaultComboBoxModel(new String[] { "0\u00B0", "+45\u00B0", "+90\u00B0", "-45\u00B0" }));
118
 
                rotationComboBox.setMaximumSize(new java.awt.Dimension(120, 20));
119
 
                rotationComboBox.setMinimumSize(new java.awt.Dimension(120, 20));
120
 
                rotationComboBox.setPreferredSize(new java.awt.Dimension(120, 20));
 
110
                rotationComboBox.setModel(new javax.swing.DefaultComboBoxModel(new String[] {
 
111
                                "0\u00B0", "+45\u00B0", "+90\u00B0", "-45\u00B0" }));
121
112
                gridBagConstraints = new java.awt.GridBagConstraints();
122
113
                gridBagConstraints.gridx = 1;
123
 
                gridBagConstraints.gridy = 5;
 
114
                gridBagConstraints.gridy = 2;
124
115
                gridBagConstraints.anchor = java.awt.GridBagConstraints.NORTHWEST;
125
116
                gridBagConstraints.insets = new java.awt.Insets(3, 3, 3, 3);
126
117
                transitionEditorPanel.add(rotationComboBox, gridBagConstraints);
161
152
 
162
153
                gridBagConstraints = new java.awt.GridBagConstraints();
163
154
                gridBagConstraints.gridx = 0;
164
 
                gridBagConstraints.gridy = 1;
 
155
                gridBagConstraints.gridy = 3;
165
156
                gridBagConstraints.anchor = java.awt.GridBagConstraints.CENTER;
166
157
                gridBagConstraints.insets = new java.awt.Insets(5, 0, 8, 3);
167
158
                add(buttonPanel, gridBagConstraints);
168
159
 
169
 
        }// </editor-fold>//GEN-END:initComponents
170
 
 
171
 
        private void nameTextFieldFocusLost(java.awt.event.FocusEvent evt) {//GEN-FIRST:event_nameTextFieldFocusLost
 
160
                nameTextField.setText(transition.getName());
 
161
                if(transition.underlyingTransition().isShared()){
 
162
                        switchToNameDropDown();
 
163
                        sharedCheckBox.setSelected(true);
 
164
                        sharedTransitionsComboBox.setSelectedItem(transition.underlyingTransition().sharedTransition());
 
165
                }else{
 
166
                        switchToNameTextField();
 
167
                }
 
168
        }
 
169
        
 
170
        private boolean hasArcsToSharedPlaces(TimedTransition underlyingTransition) {
 
171
                for(TimedInputArc arc : context.activeModel().inputArcs()){
 
172
                        if(arc.destination().equals(underlyingTransition) && arc.source().isShared()) return true;
 
173
                }
 
174
                
 
175
                for(TimedOutputArc arc : context.activeModel().outputArcs()){
 
176
                        if(arc.source().equals(underlyingTransition) && arc.destination().isShared()) return true;
 
177
                }
 
178
                
 
179
                for(TransportArc arc : context.activeModel().transportArcs()){
 
180
                        if(arc.transition().equals(underlyingTransition) && arc.source().isShared()) return true;
 
181
                        if(arc.transition().equals(underlyingTransition) && arc.destination().isShared()) return true;
 
182
                }
 
183
                
 
184
                for(TimedInhibitorArc arc : context.activeModel().inhibitorArcs()){
 
185
                        if(arc.destination().equals(underlyingTransition) && arc.source().isShared()) return true;
 
186
                }
 
187
                
 
188
                return false;
 
189
        }
 
190
 
 
191
        protected void switchToNameTextField() {
 
192
                transitionEditorPanel.remove(sharedTransitionsComboBox);
 
193
                GridBagConstraints gbc = new java.awt.GridBagConstraints();
 
194
                gbc.gridx = 1;
 
195
                gbc.gridy = 1;
 
196
                gbc.fill = java.awt.GridBagConstraints.HORIZONTAL;
 
197
                gbc.insets = new java.awt.Insets(3, 3, 3, 3);
 
198
                transitionEditorPanel.add(nameTextField, gbc);  
 
199
                transitionEditorPanel.validate();
 
200
                transitionEditorPanel.repaint();
 
201
        }
 
202
 
 
203
        protected void switchToNameDropDown() {
 
204
                transitionEditorPanel.remove(nameTextField);
 
205
                GridBagConstraints gbc = new java.awt.GridBagConstraints();
 
206
                gbc.gridx = 1;
 
207
                gbc.gridy = 1;
 
208
                gbc.fill = java.awt.GridBagConstraints.HORIZONTAL;
 
209
                gbc.insets = new java.awt.Insets(3, 3, 3, 3);
 
210
                transitionEditorPanel.add(sharedTransitionsComboBox, gbc);              
 
211
                transitionEditorPanel.validate();
 
212
                transitionEditorPanel.repaint();
 
213
        }
 
214
 
 
215
        private void nameTextFieldFocusLost(java.awt.event.FocusEvent evt) {
172
216
                focusLost(nameTextField);
173
 
        }//GEN-LAST:event_nameTextFieldFocusLost
174
 
 
175
 
        private void nameTextFieldFocusGained(java.awt.event.FocusEvent evt) {//GEN-FIRST:event_nameTextFieldFocusGained
 
217
        }
 
218
        
 
219
        private void nameTextFieldFocusGained(java.awt.event.FocusEvent evt) {
176
220
                focusGained(nameTextField);
177
 
        }//GEN-LAST:event_nameTextFieldFocusGained
178
 
 
179
 
 
180
 
        private void focusGained(javax.swing.JTextField textField){
 
221
        }
 
222
 
 
223
        private void focusGained(javax.swing.JTextField textField) {
181
224
                textField.setCaretPosition(0);
182
225
                textField.moveCaretPosition(textField.getText().length());
183
226
        }
184
227
 
185
 
        private void focusLost(javax.swing.JTextField textField){
 
228
        private void focusLost(javax.swing.JTextField textField) {
186
229
                textField.setCaretPosition(0);
187
 
        }   
 
230
        }
188
231
 
189
232
        CaretListener caretListener = new javax.swing.event.CaretListener() {
190
233
                public void caretUpdate(javax.swing.event.CaretEvent evt) {
191
 
                        JTextField textField = (JTextField)evt.getSource();
192
 
                        textField.setBackground(new Color(255,255,255));
193
 
                        //textField.removeChangeListener(this);
 
234
                        JTextField textField = (JTextField) evt.getSource();
 
235
                        textField.setBackground(new Color(255, 255, 255));
 
236
                        // textField.removeChangeListener(this);
194
237
                }
195
 
        };   
196
 
 
197
 
        private void okButtonHandler(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_okButtonHandler
198
 
 
199
 
                view.getUndoManager().newEdit(); // new "transaction""
200
 
 
 
238
        };
 
239
 
 
240
        private void okButtonHandler(java.awt.event.ActionEvent evt) {
201
241
                String newName = nameTextField.getText();
202
 
                if (!newName.equals(name)){
203
 
                        if (! Pattern.matches("[a-zA-Z]([\\_a-zA-Z0-9])*", newName)){
204
 
                                System.err.println("Acceptable names for transitions are defined by the regular expression:\n[a-zA-Z][_a-zA-Z]*");
205
 
                                JOptionPane.showMessageDialog(CreateGui.getApp(),
 
242
                        
 
243
                context.undoManager().newEdit(); // new "transaction""
 
244
                boolean wasShared = transition.underlyingTransition().isShared() && !sharedCheckBox.isSelected();
 
245
                if(transition.underlyingTransition().isShared()){
 
246
                        context.undoManager().addEdit(new UnshareTransitionCommand(transition.underlyingTransition().sharedTransition(), transition.underlyingTransition()));
 
247
                        transition.underlyingTransition().unshare();
 
248
                }
 
249
                
 
250
                if(sharedCheckBox.isSelected()){        
 
251
                        SharedTransition selectedTransition = (SharedTransition)sharedTransitionsComboBox.getSelectedItem();
 
252
                        context.undoManager().addEdit(new MakeTransitionSharedCommand(selectedTransition, transition.underlyingTransition()));
 
253
                        try{
 
254
                                selectedTransition.makeShared(transition.underlyingTransition());
 
255
                        }catch(RequireException e){
 
256
                                context.undoManager().undo();
 
257
                                JOptionPane.showMessageDialog(this,"Another transition in the same component is already shared under that name", "Error", JOptionPane.ERROR_MESSAGE);
 
258
                                return;
 
259
                        }
 
260
                }else{                  
 
261
                        if(transition.underlyingTransition().model().isNameUsed(newName) && (wasShared || !transition.underlyingTransition().name().equals(newName))){
 
262
                                context.undoManager().undo(); 
 
263
                                JOptionPane.showMessageDialog(this,
 
264
                                                "The specified name is already used by another place or transition.",
 
265
                                                "Error", JOptionPane.ERROR_MESSAGE);
 
266
                                return;
 
267
                        }
 
268
 
 
269
                        String oldName = transition.underlyingTransition().name();
 
270
                        try{ // set name
 
271
                                transition.underlyingTransition().setName(newName);
 
272
                                context.undoManager().addEdit(new RenameTimedTransitionCommand(transition.underlyingTransition(), oldName, newName));
 
273
                        }catch(RequireException e){
 
274
                                context.undoManager().undo(); 
 
275
                                JOptionPane.showMessageDialog(this,
206
276
                                                "Acceptable names for transitions are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*",
207
 
                                                "Error",
208
 
                                                JOptionPane.INFORMATION_MESSAGE);
209
 
                                return;
210
 
                        }else if ( (pnmlData.getPlaceByName(newName) != null) || (pnmlData.getTransitionByNameIgnoreGiven(transition, newName) != null) ){
211
 
                                System.err.println("Transitions cannot be called the same as an other Place or Transition.");
212
 
                                JOptionPane.showMessageDialog(CreateGui.getApp(),
213
 
                                                "Transitions cannot be called the same as another Place or Transition.",
214
 
                                                "Error",
215
 
                                                JOptionPane.INFORMATION_MESSAGE);
216
 
                                return;
217
 
                        }else {
218
 
                                view.getUndoManager().addEdit(transition.setPNObjectName(newName));
 
277
                                                "Error", JOptionPane.ERROR_MESSAGE);
 
278
                                return;
219
279
                        }
220
 
                        //        if (!(newName.charAt(0)=='#')){
221
 
                        //                if(newName.contains("*")){
222
 
                        //                        System.err.println("Transitions can't have names with *'s or +'s");
223
 
                        //                        JOptionPane.showMessageDialog(CreateGui.getApp(),
224
 
                        //                                      "Transitions can't have names with *'s or +'s\n",
225
 
                        //                                      "Error",
226
 
                        //                                      JOptionPane.INFORMATION_MESSAGE);
227
 
                        //                        return;
228
 
                        //                }else {
229
 
                        //                        view.getUndoManager().addEdit(transition.setPNObjectName(newName));
230
 
                        //                }
231
 
                        //        } else {
232
 
                        //                System.err.println("Transition can't have a name starting with #");
233
 
                        //                JOptionPane.showMessageDialog(CreateGui.getApp(),
234
 
                        //                                      "Transition can't have a name starting with #\n",
235
 
                        //                                      "Error",
236
 
                        //                                      JOptionPane.INFORMATION_MESSAGE);
237
 
                        //                        return;
238
 
                        //        }
239
 
                }      
 
280
                        context.nameGenerator().updateIndices(transition.underlyingTransition().model(), newName);
 
281
                }
240
282
 
241
283
                Integer rotationIndex = rotationComboBox.getSelectedIndex();
242
284
                if (rotationIndex > 0) {
249
291
                                angle = 90;
250
292
                                break;
251
293
                        case 3:
252
 
                                angle = 135; //-45
 
294
                                angle = 135; // -45
253
295
                                break;
254
296
                        default:
255
 
                                break;               
 
297
                                break;
256
298
                        }
257
299
                        if (angle != 0) {
258
 
                                view.getUndoManager().addEdit(transition.rotate(angle));
 
300
                                context.undoManager().addEdit(transition.rotate(angle));
259
301
                        }
260
302
                }
261
 
                transition.repaint();
262
303
                exit();
263
 
        }//GEN-LAST:event_okButtonHandler
 
304
        }
264
305
 
265
306
        private void exit() {
266
307
                rootPane.getParent().setVisible(false);
267
308
        }
268
309
 
269
 
 
270
 
        private void cancelButtonHandler(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_cancelButtonHandler
271
 
                //Provisional!
 
310
        private void cancelButtonHandler(java.awt.event.ActionEvent evt) {
272
311
                exit();
273
 
        }//GEN-LAST:event_cancelButtonHandler
274
 
 
275
 
 
276
 
        // Variables declaration - do not modify//GEN-BEGIN:variables
 
312
        }
 
313
 
277
314
        private javax.swing.JPanel buttonPanel;
278
315
        private javax.swing.JButton cancelButton;
279
316
        private javax.swing.JLabel nameLabel;
282
319
        private javax.swing.JComboBox rotationComboBox;
283
320
        private javax.swing.JLabel rotationLabel;
284
321
        private javax.swing.JPanel transitionEditorPanel;
285
 
        // End of variables declaration//GEN-END:variables
 
322
        private javax.swing.JCheckBox sharedCheckBox;
 
323
        private javax.swing.JComboBox sharedTransitionsComboBox;
286
324
 
287
325
}