On 30/10/2015 09:53, Japheth Lim wrote:
What about PolyML.SaveState.renameParent? See http://www.polyml.org/documentation/Reference/PolyMLSaveState.html
This does work for most situations but I don't find it ideal. renameParent would need to be called whenever a state file is moved. It also wouldn't work when a file is loaded through multiple paths at the same time (think e.g. a file that is shared over NFS). I propose that changing the behaviour of Poly/ML here would make it more useful.
I don't like the idea of changing the existing behaviour but there may be other alternatives. Something that occurs to me would be to provide a function to load a complete hierarchy, say PolyML.SaveState.loadHierarchy: string list -> unit
Then PolyML.SaveState.loadHierarchy["grandparent", "parent", "child"] would load a set of files. Each file currently has a signature for the parent as well as a path and these are checked in case a parent has changed so the only difference would be that the paths to all the files would be provided from ML.
David