[isabelle-dev] Hooks for postprocessing sessions!?
makarius at sketis.net
Thu Oct 11 17:40:39 CEST 2012
On Thu, 11 Oct 2012, Lars Noschinski wrote:
> On 11.10.2012 17:00, Makarius wrote:
>> 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.
> I never got around to add the whole thing to the Isabelle repository. This is
> partly related to the fact, that I only have an hackish way to hook into the
> build process and generate the index. I always wanted to revisit this. I'll
> set it on my list for after the next paper deadline.
It would be also interesting to hear how the conceptual problems of
off-line searching are addressed. At the moment we have several partial
The standard Isabelle document model -- the one being used in
Isabelle/jEdit -- is more and more taking grounds from the old HTML stuff.
There is already a function to emit one bit XML document here:
There is another function to turn external XML into the internal markup
The big conclusion of all this might be pretty close, but as I've said I
got distracted by old ML sources around find_theorems / WWW_Find. I don't
expect anything on my side before the coming release, though.
More information about the isabelle-dev