--- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Jan 28 19:23:03 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Jan 28 19:25:19 2015 +0100
@@ -61,8 +61,7 @@
val graphview =
graph_result match {
case Exn.Res(graph) =>
- val model = new isabelle.graphview.Model(graph)
- val graphview = new isabelle.graphview.Graphview(model) {
+ val graphview = new isabelle.graphview.Graphview(graph) {
def options: Options = PIDE.options.value
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =