equal
deleted
inserted
replaced
13 import java.awt.{Font, Color, Shape, Graphics2D} |
13 import java.awt.{Font, Color, Shape, Graphics2D} |
14 import java.awt.geom.{Point2D, Rectangle2D} |
14 import java.awt.geom.{Point2D, Rectangle2D} |
15 import javax.swing.JComponent |
15 import javax.swing.JComponent |
16 |
16 |
17 |
17 |
18 abstract class Graphview(val model: Model) |
18 abstract class Graphview(full_graph: Graph_Display.Graph) |
19 { |
19 { |
20 graphview => |
20 graphview => |
21 |
21 |
22 |
22 |
23 def options: Options |
23 def options: Options |
|
24 |
|
25 val model = new Model(full_graph) |
24 |
26 |
25 |
27 |
26 /* layout state */ |
28 /* layout state */ |
27 |
29 |
28 // owned by GUI thread |
30 // owned by GUI thread |