Re: [isabelle] Empty session_graph files



On Thu, 14 Apr 2016, Mathias Fleury wrote:

I found the culprit (by bisecting the commits): it is commit http://isabelle.in.tum.de/reports/Isabelle/rev/dcc8e1d34b18 <http://isabelle.in.tum.de/reports/Isabelle/rev/dcc8e1d34b18> (by Makarius Wenzel). The change is simply:
-     File.copy(graph_file, (session_prefix + Path.basic("session_graph.pdf")).file)
+     File.write(session_prefix + Path.basic("session_graph.pdf"), File.read(graph_file))

Does anyone understand what is going on here? The two commands generates files with different sizes (File.write generates a longer file than File.copy).

Thanks for figuring out this drop-out from last October.

This is a typical Unicode accident: File.read and File.write operate on type string in ML and String in Scala, but the latter only works for text (in UTF8 encoding). Thus the non-text PDF is messed up.

So I need to go back to File.copy and ensure that reasonable file permissions are produced by other means.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.