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 model = new isabelle.graphview.Model(graph) |
65 val visualizer = new isabelle.graphview.Visualizer(model) { |
65 val visualizer = new isabelle.graphview.Visualizer(model) { |
66 override def foreground_color = view.getTextArea.getPainter.getForeground |
|
67 override def background_color = view.getTextArea.getPainter.getBackground |
|
68 override def selection_color = view.getTextArea.getPainter.getSelectionColor |
|
69 override def error_color = PIDE.options.color_value("error_color") |
|
70 override def font_size = view.getTextArea.getPainter.getFont.getSize |
|
71 override def font = view.getTextArea.getPainter.getFont |
|
72 } |
|
73 new isabelle.graphview.Main_Panel(model, visualizer) { |
|
74 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 = |
75 { |
67 { |
76 Pretty_Tooltip.invoke(() => |
68 Pretty_Tooltip.invoke(() => |
77 { |
69 { |
78 val rendering = Rendering(snapshot, PIDE.options.value) |
70 val rendering = Rendering(snapshot, PIDE.options.value) |
79 val info = Text.Info(Text.Range(~1), body) |
71 val info = Text.Info(Text.Range(~1), body) |
80 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) |
72 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) |
81 }) |
73 }) |
82 null |
74 null |
83 } |
75 } |
|
76 override def foreground_color = view.getTextArea.getPainter.getForeground |
|
77 override def background_color = view.getTextArea.getPainter.getBackground |
|
78 override def selection_color = view.getTextArea.getPainter.getSelectionColor |
|
79 override def error_color = PIDE.options.color_value("error_color") |
|
80 override def font_size = view.getTextArea.getPainter.getFont.getSize |
|
81 override def font = view.getTextArea.getPainter.getFont |
84 } |
82 } |
|
83 new isabelle.graphview.Main_Panel(model, visualizer) |
85 case Exn.Exn(exn) => new TextArea(Exn.message(exn)) |
84 case Exn.Exn(exn) => new TextArea(Exn.message(exn)) |
86 } |
85 } |
87 set_content(graphview) |
86 set_content(graphview) |
88 |
87 |
89 override def init() |
88 override def init() |