equal
deleted
inserted
replaced
59 } |
59 } |
60 |
60 |
61 val graphview = |
61 val graphview = |
62 graph_result match { |
62 graph_result match { |
63 case Exn.Res(graph) => |
63 case Exn.Res(graph) => |
64 val model = new isabelle.graphview.Model(graph) |
64 val graphview = new isabelle.graphview.Graphview(graph) { |
65 val graphview = new isabelle.graphview.Graphview(model) { |
|
66 def options: Options = PIDE.options.value |
65 def options: Options = PIDE.options.value |
67 |
66 |
68 override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
67 override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
69 { |
68 { |
70 Pretty_Tooltip.invoke(() => |
69 Pretty_Tooltip.invoke(() => |