[isabelle-dev] Improved Graphview

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Jan 23 19:38:01 CET 2015


>> Attentive readers of incoming changesets might have noticed the recent
>> improvements of the Graphview component, which was a not-quite-working
>> student project from some years ago.
>>
> More details are present in Isabelle/5d08b2332b76, notably some kind of
> "tree view" on the content, with possibilities to select a subset of
> nodes, or jump to a particular node via double-click.

Great!  With this is it now possible e.g. to analyze all additive type
classes using sth like

	class_deps (zero | plus | minus | uminus)

and then »Show content«.

> I haven't used the locale dependency graph much, just a bit in
> 533f6cfc04c0 (with the new Graphview component).

I guess you are referring to »locale_deps« here.

This is just an approximation of something how a visualization of locale
dependencies could look one day.  Open issues include:
* What is the semantics of an edge?  Is it something like »regular
import« (as opposite to »mixin import«)?
* How to represent mixin imports?  As explicit statement?  As annotated
edges (but cycles make problems here)?

I would really appreciate progress here, but the graph browser issue
seems to stand as something apart from that.

	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: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150123/19f2786a/attachment.sig>


More information about the isabelle-dev mailing list