Re: [isabelle] Thy_Load structure don't exists for Windows



I got your idea Makarius and you explained me that before.

My point by saying the line "ThyLoad ~> Thy_Load" is useless was to mention
that:
If a given change on a function or a module was relevant why at some point
changes happen on the same thing with the assumption that it is not
relevant anymore.

>The
>master_directory has actually become a bit less relevant to Isabelle/ML
>user codes, because Resources.parse_files and
>Resources.provide_parse_files have taken over the details of managing
>external sources in a way that also works with the Prover IDE

But the above paragraph of your reply explain why it becomes irrelevant.

By the way I am porting my old theories containing ML code to the latest
version that is why I faced this change.



2016-12-16 13:36 GMT-05:00 Makarius <makarius at sketis.net>:

> On 15/12/16 22:16, Nemouchi Yakoub wrote:
> >
> > In Isabelle 2016 the structure Thy_Load  does not exist (at least for
> > Windows distribution).
> >
> > The function Thy_Load.master_directory is renamed
> >  Resources.master_directory
> >
> > No of these changes are mentioned in the NEWS.
>
> Do you mean Isabelle2016 (February 2016) or the current Isabelle2016-1
> (December 2016)? Anyway, the renaming of structure Thy_Load to Resources
> happened between Isabelle2013-2 (December 2013) and Isabelle2014 (August
> 2014):
> http://isabelle.in.tum.de/repos/isabelle/rev/06cc31dff138
>
>
> The NEWS file covers only "history of user-relevant changes", while the
> true history is managed by Mercurial. Both need to be consulted
> occasionally.
>
> Not every small change ends up in NEWS: the above could have been added
> or not, depending on an estimate how user-relevant it really is. The
> master_directory has actually become a bit less relevant to Isabelle/ML
> user codes, because Resources.parse_files and
> Resources.provide_parse_files have taken over the details of managing
> external sources in a way that also works with the Prover IDE (but that
> important change is not document either -- it needs to be derived from
> the typical uses in the sources).
>
>
> > And imao this line: "ThyLoad ~> Thy_Load" in the NEWS file is useless the
> > structure does not even exist.
>
> NEWS contains the cumulative (immutable) history of user-relevant
> changes. The renaming of "ThyLoad ~> Thy_Load" belongs to Isabelle2009-2
> (June 2010). This can be seen in the SideKick tree view of
> Isabelle/jEdit -- the NEWS file says in the very beginning:
>
>   Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.
>
> I find it very hard to work without the Prover IDE these days. It is
> relevant for the NEWS file, ROOT files, ML files, thy files ...
>
>
>         Makarius
>
>
>



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