~tapaal-maintainers/tapaal/3.4

« back to all changes in this revision

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

  • Committer: Jiri Srba
  • Date: 2018-05-11 14:53:50 UTC
  • Revision ID: srba@cs.aau.dk-20180511145350-ay8p84sw0rrn8jc1
merged in branch lp:~tapaal-contributor/tapaal/Rename-transition-error-1767489
fixing a non-cought expection in transition name renaming

Show diffs side-by-side

added added

removed removed

Lines of Context:
423
423
                                return false;
424
424
                        }
425
425
 
426
 
                        String oldName = transition.underlyingTransition().name();
427
 
                        transition.underlyingTransition().setName(newName);
428
 
                        Command renameCommand = new RenameTimedTransitionCommand(context.tabContent(), transition.underlyingTransition(), oldName, newName);
429
 
                        context.undoManager().addEdit(renameCommand);
430
 
                        try{ // set name
 
426
                        try{ 
 
427
                                String oldName = transition.underlyingTransition().name();
 
428
                                transition.underlyingTransition().setName(newName);
 
429
                                Command renameCommand = new RenameTimedTransitionCommand(context.tabContent(), transition.underlyingTransition(), oldName, newName);
 
430
                                context.undoManager().addEdit(renameCommand);
 
431
                                // set name
431
432
                                renameCommand.redo();
432
433
                        }catch(RequireException e){
433
434
                                context.undoManager().undo();