[isabelle-dev] Directory layout

[Makarius]

On Mon, 1 Dec 2008, Florian Haftmann wrote:

> The switch to hg makes it possible to adapt some file locations (file
> names) in the Isabelle distribution which have evolved over time but do
> not fit to the logical structure of the distribution any longer,
> according to the following table:
> 
>     src/Provers/* ~> src/Tools/*
>     src/Pure/Tools/* ~> src/Tools/*
> 
>     src/HOL/arith_data.ML ~> src/HOL/Tools
>     src/HOL/hologic.ML ~> src/HOL/Tools
>     src/HOL/simpdata.ML ~> src/HOL/Tools

I cannot really say much about HOL, you know better about its logical 
structure.

Concerning src/Provers, src/Tools, src/Pure/Tools:

  * The distinction of src/Provers and src/Tools is mostly nostalgic, so 
    Provers should go into Tools.  For quite some time, we have already 
    followed the convention of putting new things in src/Tools.

  * The role of src/Pure/Tools is still unclear.  The difference is that 
    these are actually loaded into the Pure image, and all its 
    contributing sources should be in src/Pure.  I would say we leave 
    src/Pure/Tools unchanged for now until we get a better idea.

BTW, moving files will also affect manuals.  In the newer ones (isar-ref, 
system, implementation) I have already used the @{file} document 
antiquotation to get a statically checked references to the Isabelle file 
space.


	Makarius