changeset 59462 | c7eff4356885 |
parent 59460 | 3a357fef24e8 |
child 61176 | 9791f631c20d |
--- a/src/Tools/Graphview/graphview.scala Wed Jan 28 19:23:03 2015 +0100 +++ b/src/Tools/Graphview/graphview.scala Wed Jan 28 19:25:19 2015 +0100 @@ -15,13 +15,15 @@ import javax.swing.JComponent -abstract class Graphview(val model: Model) +abstract class Graphview(full_graph: Graph_Display.Graph) { graphview => def options: Options + val model = new Model(full_graph) + /* layout state */