[isabelle-dev] usedir -P P "http://isabelle.in.tum.de/library/"

[Makarius]

On Sat, 1 Sep 2012, Gerwin Klein wrote:

> How do I do the equivalent of "isabelle usedir -P URL" in the new build 
> system?
>
> I'm trying to make sure that generated HTML for AFP entries doesn't 
> contain dangling links of the form "up to index of HOL/HOLCF"
>
> Basically, only the HTML for AFP entries should be on the AFP site, the 
> rest should link back to the distribution. I'm not sure where/how to say 
> which sessions should generate back links and which not and I couldn't 
> find anything enlightening in isabelle options.

The -P option never worked out beyond the situation where some body of 
Isabelle applications points back to some background distribution.  There 
was a lack of version-awareness and further add-ons in the hierarchy of 
applications (longer chains of back-references).

Before not upgrading the old -P feature to the current build tool, I 
actually spent some thoughts how AFP would manage without it.  You 
basically just need to do the normal build including the "base sessions", 
so the browser_info for these will accumulate in the right spot to be 
linked correctly.

Thus even an unidentified development snapshot like 
http://afp.sourceforge.net/browser_info/devel/HOL/Datatype_Order_Generator/Order_Generator.html 
would point to the correct version of Main -- the one that was used to 
build it -- not the one that happens to be on the official Isabelle 
website.


Apart from nostalgy about discontinued options, there is actually a an 
oddity left in the way browser_info is organized: its directory structure 
follows the tree of session images, but that leads to a slightly 
unorganized situation in practice.  I still did not find the spot in the 
AFP scripts where the location of the generated HTML files is guessed. 
This might be a starting point for further reforms that clarify the 
situation further, say with some explicit sectioning within AFP, and in 
contrast to what it uses from the background.


 	Makarius