Re: [isabelle-dev] Improved Graphview
Here is another small stepping stone: Isabelle/e82c72f3b227. The Isabelle/Scala graph layout is now used to produce the session_graph.pdf for document preparation. Moreover the same output is used for theory dependencies in HTML, and the old GraphBrowser applet has been discontinued. What is still remaining is the old browser alternative of thy_deps, locale_deps, class_deps, thm_deps, code_deps. It is not fully superseded by the new graphview yet, because the latter still lacks possibilities to fold subgraphs (according to hierarchical tree structure of the name space, or all preds/succs within the graph dependencies). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Improved Graphview
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
Re: [isabelle-dev] Improved Graphview
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. 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. Great! With this is it now possible e.g. to analyze all additive type classes using sth like class_deps (zero | plus | minus | uminus) and then »Show content«. I haven't used the locale dependency graph much, just a bit in 533f6cfc04c0 (with the new Graphview component). I guess you are referring to »locale_deps« here. This is just an approximation of something how a visualization of locale dependencies could look one day. Open issues include: * What is the semantics of an edge? Is it something like »regular import« (as opposite to »mixin import«)? * How to represent mixin imports? As explicit statement? As annotated edges (but cycles make problems here)? I would really appreciate progress here, but the graph browser issue seems to stand as something apart from that. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Improved Graphview
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Improved Graphview
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Improved Graphview
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. I hope to wrap it up eventually for the coming release (this Spring) -- like various other things that are still in the pipeline and got delayed as usual (e.g. important reforms for Eisbach). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
