[isabelle-dev] Hooks for postprocessing sessions!?
makarius at sketis.net
Thu Oct 11 17:00:09 CEST 2012
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
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.
More information about the isabelle-dev