Changing the name of .mlw files
Hello,
I think it could be useful to have a way to safely rename *.mlw files once a proof is started (preferably from the ide or from the API [maybe for SPARK]). Can why3session be used for this ?
Here is what I tried:
- create a.mlw:
module Todo goal g: true end
mv a.mlw b.mlw
-
- start why3ide from directory a: an error occurs (note that I think it should only says that the session file is detached not return an error)
- move directory a to directory b and starts from b (a.mlw is still detached because part of the session)
- start from b.mlw: the part about a.mlw is detached and I "lost" (I can copy/paste) my proof in a
- manually edit the session file name (I want to avoid that: also do I need to update shapes too ?)
Do you have an idea of what I should do/what could be done or improved ?