Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Changes to ML File structure in Isabelle2016-RC0


view this post on Zulip Email Gateway (Aug 22 2022 at 12:07):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Sorry if this is supposed to be obvious, but...

I have some ML code that I am using the Isabelle/JEdit interface with.
The code all works with Isabelle 2015, but in Isabelle2016-RC0 I see
an incompatible change to the File structure, where File.open_input
takes BinIO.instream -> 'a instead of TextIO.instream -> 'a.

Where can I find the documentation of these changes? I am sorry,
I have forgotten where I found any documentation when I originally
did this a year or two ago. Thanks!

- Gene Stark

view this post on Zulip Email Gateway (Aug 22 2022 at 12:07):

From: Makarius <makarius@sketis.net>
Usually in the NEWS, but such tiny things do not always show up there.
In such cases the place to look is the history:
http://isabelle.in.tum.de/repos/isabelle/rev/67e389f67073

That changeset provides further explanations and examples how to convert
existing applications.

Makarius


Last updated: Apr 25 2024 at 12:23 UTC