<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Hi Florian,<br>
    <br>
    Thanks for your feedback. The main developer Markus Kaiser is giving
    a presentation next week and we will discuss further steps.<br>
    <br>
    Here's a part of a private German discussion with Makarius that
    explains how to switch back to the classical browser (in PG/Emacs).<br>
    <br>
    in <a class="moz-txt-link-freetext"
      href="http://isabelle.in.tum.de/repos/isabelle/rev/7529c77ee92e">http://isabelle.in.tum.de/repos/isabelle/rev/7529c77ee92e</a>
    ist nun alles erstmal integriert.  Einige Sachen funktionieren aber
    noch nicht so glatt, z.B. ein voller class_deps graph von HOL/Main. 
    Das eine oder andere Detail habe ich möglicherweise auch kaputt
    gemacht.
    <br>
    <br>
    Man kann in isabelle tty oder emacs mit der print mode option "-m
    graphview" das neue Tool aktivieren, sonst wird wie bisher der alte
    browser verwendet.  Das gilt einheitlich für alle commands die
    intern auf display_graph basieren. Isabelle/jEdit verwendet stets
    Graphview in einem eigenen Dockable Window -- auch wenn das noch
    nicht Produktionsqualität erreicht.
    <br>
    <br>
    <br>
    Lukas<br>
    <br>
    <br>
    On 10/11/2012 01:31 PM, Florian Haftmann wrote:
    <blockquote cite="mid:5076AE25.4040909@informatik.tu-muenchen.de"
      type="cite">
      <pre wrap="">Hi all,

the recently established graphview IMHO has currently two disadvantages:
* Misfit of node annotation size wrt. to the size of the full graphs –
node annotations are not readable within a reasonable size coverage of
the graph.
* Does not scale well (e.g. class_deps from Main.thy).

What are the plans for the next release?  Graph browsing is a tool too
vital that it can be set inoperative.  Is there any chancing for
improvements, or will there be a switch towards the classical browser
alternatively?

Cheers,
        Florian

</pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>