[isabelle-dev] Graphview

[Makarius]

On Thu, 11 Oct 2012, Florian Haftmann wrote:

>> The class_deps non-scalability probably stems from the omission of the
>> transitive reduction (Hasse diagram).  This was probably done due to the
>> anticipated locale graph visualization (which does not quite work), or
>> it might be just an omission.
>
> The latter.  I am not aware of any locale graph visualization apart from
> a sketch two (?) years ago on the mailing list.

The result is called Graphview now.  The 'locale_deps' command will give 
you the locale aspect of it, but the result is not very usable at the 
moment.

A side question here: Is there a sensible way to make 'print_locale' 
informative about its axiomatic basis, or its view in terms of the goal 
presented in interpretation.

See also changeset 7b6aaf446496, where I trashed your earlier attempt at 
it without looking very closely at it -- the priority was to unify the 
pretty output / pretty tooltip model and get rid of hardwired "locale" 
content of the graphview tool.


 	Makarius