~tapaal-developers/tapaal/trunk

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java

merged in  lp:~tapaal-contributor/tapaal/hide-show-names-1921393 allowing to show/hide place/transition names

Show diffs side-by-side

added added

removed removed

Lines of Context:
22
22
        public void redo() {
23
23
                place.setName(newName);
24
24
                updateQueries(oldName, newName);
25
 
        }
 
25
    }
26
26
 
27
27
        @Override
28
28
        public void undo() {
29
29
                place.setName(oldName);
30
30
                updateQueries(newName,oldName);
31
 
        }
 
31
    }
32
32
        
33
33
        private void updateQueries(String nameToFind, String nameToInsert){
34
34
                RenamePlaceTCTLVisitor renameVisitor = new RenamePlaceTCTLVisitor(nameToFind, nameToInsert);