On 26/12/2018 13:45, David Matthews wrote: > > However, the table itself is really a relic of some very old code and > the whole thing needs to be replaced. The table does two things. One > is to ensure that streams are not persistent [...] The other use of the table > is to > enable streams to be garbage-collected: i.e. if a stream is no longer > reachable then at some point the stream will be closed. > > Achieving non-persistence is easy as a result of some recent changes. > Garbaging-collecting streams is more difficult. Does anyone actually > rely on streams being garbage-collected? Would doing away with that and > requiring streams to be closed explicitly cause any problems?
I was not aware of such an auto-close feature via garbage collection, and I guess that the Isabelle/ML infrastructure is sufficiently robust in closing its streams properly. Incidently, I have recently tried to make this even more robust wrt. events from the environment (interrupt exceptions), see change http://isabelle.in.tum.de/repos/isabelle/rev/023d92df3d84 "more robust open/close bracket, but with potential danger of blocking indefinitely in uninterruptible state". The idea is to ensure that the "stream open" state cannot be interrupted and is always followed by explicit "close" operations. Reconsidering this again, I am unsure if the uninterruptible "open" is really such a good idea: it implicitly assumes that failed attempts at a remote connection (e.g. network file-system or socket) do not block indefinitely, but cause a timeout eventually. Makarius _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
