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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
