equal
deleted
inserted
replaced
35 /* GUI components */ |
35 /* GUI components */ |
36 |
36 |
37 private val graphview = new JPanel |
37 private val graphview = new JPanel |
38 |
38 |
39 // FIXME mutable GUI content |
39 // FIXME mutable GUI content |
40 private def set_graphview(snapshot: Document.Snapshot, graph: XML.Body) |
40 private def set_graphview(snapshot: Document.Snapshot, graph_xml: XML.Body) |
41 { |
41 { |
|
42 val graph = isabelle.graphview.Model.decode_graph(graph_xml).transitive_reduction_acyclic |
|
43 |
42 graphview.removeAll() |
44 graphview.removeAll() |
43 graphview.setLayout(new BorderLayout) |
45 graphview.setLayout(new BorderLayout) |
44 val panel = |
46 val panel = |
45 new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) { |
47 new isabelle.graphview.Main_Panel(graph) { |
46 override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
48 override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
47 { |
49 { |
48 val rendering = Rendering(snapshot, PIDE.options.value) |
50 val rendering = Rendering(snapshot, PIDE.options.value) |
49 new Pretty_Tooltip(view, parent, rendering, x, y, body) |
51 new Pretty_Tooltip(view, parent, rendering, x, y, body) |
50 null |
52 null |