[isabelle-dev] Improved Graphview

[Lars Noschinski]

On 18.01.2015 23:14, Makarius wrote:
> On Sat, 17 Jan 2015, Makarius wrote:
>
>> 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.
>>
>> As of Isabelle/32b162d1d9b5 it is already quite usable, although a
>> few details of the old graph browser are still missing.
>
> 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.
>
> I am leaving a brief time-window open to point out "remaining uses of
> the old browser", but the plan is to dismantle it rather soon.
I haven't used the locale dependency graph much, just a bit in
533f6cfc04c0 (with the new Graphview component).

While the UI was clearly subobtimal, I found it very useful to be able
to show only a part of the total graph (via "Show -> only children" or
so). Similarly, I liked the ability to highlight the children/parents of
certain nodes.

I'll describe the use-case: I have a hierarchy of 19 locales, with 1
root and 8 leaves, describing some complex case distinction. After 
finishing the proof I got the certain feeling that this hierarchy is too
complex or not enough partial results are shared. So, I'm only
interested in this part of the whole locale hierarchy

  --> I don't want to see any other nodes

Furthermore, I have a property P and in my hierarchy there locales
corresponding to P and not P. I wanted to ensure that each of my leaf
locales inherited from one of these locales (the structure was very much
a DAG, not really tree-like, so it was not obvious to see).

  --> I colored the descendants of the P and not-P locales (bonus points
for different colors).

I then proceeded to print the resulting graph and adding further
annotations with a pen ;)

  -- Lars