[isabelle-dev] Improved Graphview

Lars Noschinski noschinl at in.tum.de
Wed Jan 21 12:08:24 CET 2015


On 21.01.2015 11:58, Lars Noschinski wrote:
> 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 ;)
I just tried it again with fde2659085e1. Without the ability to filter
out irrelevant nodes, the task described here feels rather daunting



More information about the isabelle-dev mailing list