Merge lp:~tapaal-contributor/tapaal/undo-annotation-note-1834460 into lp:tapaal

[Peter Haahr Taankvist]

Undo annotation note now works on first ctrl+z

[Jiri Srba (srba)]

Fixes the problem.

review: Approve

=== modified file 'src/pipe/gui/graphicElements/AnnotationNote.java'
--- src/pipe/gui/graphicElements/AnnotationNote.java	2019-03-13 07:27:29 +0000
+++ src/pipe/gui/graphicElements/AnnotationNote.java	2019-09-21 07:52:02 +0000
@@ -167,7 +167,7 @@
 		String newText = note.getText();
 		if (oldText != null && !newText.equals(oldText)) {
 			// Text has been changed
-			CreateGui.getDrawingSurface().getUndoManager().addNewEdit(
+			CreateGui.getDrawingSurface().getUndoManager().addEdit(
 					new AnnotationTextEdit(this, oldText, newText));
 			updateBounds();
 		}
 
=== modified file 'src/pipe/gui/undo/AddPetriNetObjectEdit.java'
--- src/pipe/gui/undo/AddPetriNetObjectEdit.java	2011-09-22 14:51:36 +0000
+++ src/pipe/gui/undo/AddPetriNetObjectEdit.java	2019-09-21 07:52:02 +0000
@@ -31,12 +31,14 @@
 	@Override
 	public void undo() {
 		pnObject.delete();
+		view.repaint();
 	}
 
 	/** */
 	@Override
 	public void redo() {
 		pnObject.undelete(view);
+		view.repaint();
 	}
 
 	@Override