equal
deleted
inserted
replaced
44 def box_gap: Double = gap.ceil |
44 def box_gap: Double = gap.ceil |
45 def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil |
45 def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil |
46 } |
46 } |
47 } |
47 } |
48 |
48 |
49 class Visualizer(val model: Model) |
49 class Visualizer(options: => Options, val model: Model) |
50 { |
50 { |
51 visualizer => |
51 visualizer => |
52 |
52 |
53 |
53 |
54 /* tooltips */ |
54 /* tooltips */ |
65 def dummy_color: Color = Color.GRAY |
65 def dummy_color: Color = Color.GRAY |
66 |
66 |
67 |
67 |
68 /* font rendering information */ |
68 /* font rendering information */ |
69 |
69 |
70 def font_size: Int = 12 |
70 def font(): Font = |
71 def font(): Font = new Font("Helvetica", Font.PLAIN, font_size) |
71 { |
|
72 val family = options.string("graphview_font_family") |
|
73 val size = options.int("graphview_font_size") |
|
74 new Font(family, Font.PLAIN, size) |
|
75 } |
72 |
76 |
73 val rendering_hints = |
77 val rendering_hints = |
74 new RenderingHints( |
78 new RenderingHints( |
75 RenderingHints.KEY_ANTIALIASING, |
79 RenderingHints.KEY_ANTIALIASING, |
76 RenderingHints.VALUE_ANTIALIAS_ON) |
80 RenderingHints.VALUE_ANTIALIAS_ON) |