[isabelle-dev] Hooks for postprocessing sessions!?

[Makarius]

On Thu, 11 Oct 2012, Lukas Bulwahn wrote:

> this sounds similar to ideas that (Alex and) Lars had to allow 
> find_theorems to search on all Isabelle sessions. As far as I know, they 
> have an implementation for this feature in their shelf.

I was wondering about that recently.  So far the only visible result was 
an unclear status of find_theorems.ML (e.g. in Isabelle/e3945ddcb9aa). 
At some point I would like to see find_theorems.scala as well.


Concerning HTML processing and add ons: as a result of some changes due to 
the new build tool, there are still some loose ends.  I was considering 
more drasting renovations, like moving the functionality into 
Isabelle/Scala, but did not get very far.  I got stuck with WWW_Find and 
the question of its dependence on old HTML functionality, which is not 
immediately clear.

My present plan for the release was to put classic HTML generation just 
into the old form again, such that the index looks more ordered and the 
session information appears in the proper directories.  I also need to 
update the Admin scripts to produce the HTML library for release.


 	Makarius