[isabelle-dev] Hooks for postprocessing sessions!?

[Makarius]

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 
online solutions.


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: 
http://isabelle.in.tum.de/repos/isabelle/file/bb5db3d1d6dd/src/Pure/PIDE/document.scala#l477
There is another function to turn external XML into the internal markup 
tree.

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.


 	Makarius