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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
