equal
deleted
inserted
replaced
7 package isabelle.graphview |
7 package isabelle.graphview |
8 |
8 |
9 import isabelle._ |
9 import isabelle._ |
10 |
10 |
11 import java.awt.{RenderingHints, Graphics2D} |
11 import java.awt.{RenderingHints, Graphics2D} |
|
12 import javax.swing.JComponent |
12 |
13 |
13 |
14 |
14 class Visualizer(val model: Model) { |
15 class Visualizer(val model: Model) { |
15 object Coordinates { |
16 object Coordinates { |
16 private var nodes = Map[String, (Double, Double)]() |
17 private var nodes = Map[String, (Double, Double)]() |
141 else k.split('.').last |
142 else k.split('.').last |
142 } |
143 } |
143 |
144 |
144 object Tooltip { |
145 object Tooltip { |
145 def content(name: String): XML.Body = model.complete.get_node(name).content |
146 def content(name: String): XML.Body = model.complete.get_node(name).content |
|
147 } |
146 |
148 |
147 def text(name: String, fm: java.awt.FontMetrics): String = // null |
|
148 { |
|
149 val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm)) |
|
150 if (txt == "") null |
|
151 else |
|
152 "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " + |
|
153 Parameters.font_size + "px; \">" + // FIXME proper scaling (!?) |
|
154 HTML.encode(txt) + "</pre></html>" |
|
155 } |
|
156 } |
|
157 |
|
158 object Font { |
149 object Font { |
159 import java.awt.{Font => awtFont} |
150 import java.awt.{Font => awtFont} |
160 |
151 |
161 def apply() = new awtFont(Parameters.font_family, |
152 def apply() = new awtFont(Parameters.font_family, |
162 awtFont.BOLD, Parameters.font_size) |
153 awtFont.BOLD, Parameters.font_size) |