63 graph match { |
63 graph match { |
64 case Exn.Res(proper_graph) => |
64 case Exn.Res(proper_graph) => |
65 new isabelle.graphview.Main_Panel(proper_graph) { |
65 new isabelle.graphview.Main_Panel(proper_graph) { |
66 override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
66 override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
67 { |
67 { |
68 val rendering = Rendering(snapshot, PIDE.options.value) |
68 Pretty_Tooltip.invoke(() => |
69 val screen_point = new Point(x, y) |
69 { |
70 SwingUtilities.convertPointToScreen(screen_point, parent) |
70 val rendering = Rendering(snapshot, PIDE.options.value) |
71 Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, body) |
71 val screen_point = new Point(x, y) |
|
72 SwingUtilities.convertPointToScreen(screen_point, parent) |
|
73 Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, body) |
|
74 }) |
72 null |
75 null |
73 } |
76 } |
74 } |
77 } |
75 case Exn.Exn(exn) => new TextArea(Exn.message(exn)) |
78 case Exn.Exn(exn) => new TextArea(Exn.message(exn)) |
76 } |
79 } |