[isabelle-dev] Hooks for postprocessing sessions!?

[Florian Haftmann]

Hi all,

recently I had the idea to generate reports for all accessible Isabelle
sessions containing e.g.

* all constants (with types) declared in a session
* all types declared in a session
* all classes declared in a session
* all theorems declared via »theorem«
* …

The rationale is that this would allow for a quick analysis especially
of the AFP to find out which generally useful »auxiliary« stuff is
hidden there (e.g.
http://afp.hg.sourceforge.net/hgweb/afp/afp/file/e9fa38f86b76/thys/Binomial-Heaps/SkewBinomialHeap.thy#l1643).

Is there already feasible hook interface to hook in, e.g. in present.ML,
or can this only be done by an ad-hoc patch?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121011/d2fad446/attachment.asc>