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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
