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 <> (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"),

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: 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.


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