Re: [isabelle] Empty session_graph files



Hi,

Am Donnerstag, den 14.04.2016, 11:38 +0200 schrieb Makarius:
> 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 ; (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.


I just noticed an empty session graph here as well, probably due to the
same reason.

Is there a way to get a session graph with Isabelle 2016 (without
applying a, eh, local code change to it)?

Greetings,
Joachim

-- 

Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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