[isabelle-dev] Improved Graphview

[Makarius]

On Wed, 21 Jan 2015, 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 ;)

At least printing should now work properly via PDF.

Are more than one special colors really required?  I am presently 
considering to improve the "selection" concept (similar to the regular 
text editor selection and its current line/caret), but to discontinue the 
extra colors (which are presently de-activated in e82c72f3b227).

Concerning show/hide of sub-graphs, I have also disabled the earlier 
attempt for now, because it was conceptually not right, and leading to 
strange crashes.  It needs further cleanup, as already done for most of 
the remaining code.


The general plan for the coming release is this:

   * Put the new graphview into a shape such that the old browser can be
     deleted without any regrets (nor nostalgy about Java 1.1 AWT).

   * Add a few small things beyond the status-quo of the old browser, e.g.
     like the "Show content" mode that is already there.

There are many more possibilities beyond that.  Proper locale_deps 
visualisation has already been pointed out by Florian, although that would 
have to treat cyclic graphs, which is presently not supported.


 	Makarius