ML support for generic graph display, with browser and graphview backends (via print modes);
reverse graph layout (again), according to the graph orientation provided by ML;
simplified scala types -- eliminated unused type parameters;
more explicit Model.Info, Model.Graph;
renamed isabelle.graphview.Graphview_Frame to isabelle.graphview.Frame in accordance to file name;
removed obsolete Graph_XML and Tooltips;
tuned graphview command line;
more generous JVM resources via GRAPHVIEW_JAVA_OPTIONS;
/* Title: Tools/Graphview/src/mutator_event.scala
Author: Markus Kaiser, TU Muenchen
Events for dialog synchronization.
*/
package isabelle.graphview
import java.awt.Color
object Mutator_Event
{
type Mutator_Markup = (Boolean, Color, Mutator)
sealed abstract class Message
case class Add(m: Mutator_Markup) extends Message
case class NewList(m: List[Mutator_Markup]) extends Message
}