Implement detached nodes
The detached mechanism is not working. Detached would be used when transformations fails during reloads or when their subgoals change. Currently, if a transformation fails at reload the corresponding subproof tree is lost. With detached nodes, one would be able to reuse proof that were working before to adapt new proofs.
In this issue, several parts should be checked/done:
- change the structure of session_itp: detached should be a boolean (like obsolete) not separated lists. Because the detached status depends from the tasks: it does not make sense during the loading of a session, it only makes sense during the merge,
- when a transformation fails at reload, it should appear in the interface as detached (probably enough to add a try/with in add_registered_transformation around apply_transform_arg and add failed transformations to the parent for the session side),
- transformations missed during merge should not be lost but detached instead,
- interactivity with detached object in IDE (remove/copy/paste etc).