#319 Easy renaming with org.rodinp.core.IElementManipulation.move()
When calling IElementManipulation.move(), one may want to rename the moved element so as to avoid name collision.
However with the current API, as of Rodin 2.8, the caller has to provide the new name, without access to the internal fresh name generator used by org.rodinp.core.IInternalElement.createChild().
So we end up replacing a call to move() by 2 calls: createChild() and then delete() to get the desired result, potentially breaking operation atomicity.
There are actually 4 name collision handling options we could provide in a new API:
- override previous element
- throw an exception
- rename automatically (using internal fresh name generator)
- rename with caller given name (although this option probably becomes useless when given the previous one)
Moreover, after calling move() on an element with a different parent, calling getParent() on the moved element still returns the original parent, which is disturbing and error-prone. The moved element has just become a mere handle to a non existing element.
If there is any good reason for that, it deserves documentation, and the move() method should return the new existing moved element that has the new parent.
Just to added that I was desparated for the third option (rename automatically) not so long ago, and ended up doing createChild() and move() with overriding flag set to "true".
Cheers,
Son