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



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.