[isabelle-dev] Improved Graphview
noschinl at in.tum.de
Wed Jan 21 11:58:08 CET 2015
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
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 ;)
More information about the isabelle-dev