~tapaal-contributor/tapaal/unselect-objects-after-undo-1894108

« back to all changes in this revision

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

- Did some refactorings in the model.
- Added double click shortcut to shared places/transitions list.

Show diffs side-by-side

added added

removed removed

Lines of Context:
76
76
                                                                .getPoint());
77
77
                                                ListModel dlm = constantsList.getModel();
78
78
                                                Constant c = (Constant) dlm.getElementAt(index);
79
 
                                                ;
80
79
                                                constantsList.ensureIndexIsVisible(index);
81
80
 
82
81
                                                showEditConstantDialog(c);