editor.updateHistory();
editor.updateTitle();
    public synchronized void undo() throws CannotUndoException {        super.undo();        updateActions();        editor.updateHistory();        // todo: Updating of the mapview should ultimately happen        // todo: automatically based on the changes made to the map.        editor.getMapView().repaint();    }