equal
deleted
inserted
replaced
84 |
84 |
85 /* component state -- owned by Swing thread */ |
85 /* component state -- owned by Swing thread */ |
86 |
86 |
87 private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty |
87 private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty |
88 |
88 |
89 private class Node_Renderer_Component extends Label |
89 private object Node_Renderer_Component extends Label |
90 { |
90 { |
|
91 opaque = false |
91 xAlignment = Alignment.Leading |
92 xAlignment = Alignment.Leading |
92 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
93 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
93 |
94 |
94 var node_name = Document.Node.Name.empty |
95 var node_name = Document.Node.Name.empty |
95 override def paintComponent(gfx: Graphics2D) |
96 override def paintComponent(gfx: Graphics2D) |
116 } |
117 } |
117 super.paintComponent(gfx) |
118 super.paintComponent(gfx) |
118 } |
119 } |
119 } |
120 } |
120 |
121 |
121 private class Node_Renderer extends |
122 private class Node_Renderer extends ListView.Renderer[Document.Node.Name] |
122 ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component]( |
|
123 new Node_Renderer_Component) |
|
124 { |
123 { |
125 def configure(list: ListView[_], isSelected: Boolean, focused: Boolean, |
124 def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, |
126 name: Document.Node.Name, index: Int) |
125 name: Document.Node.Name, index: Int): Component = |
127 { |
126 { |
128 component.opaque = false |
127 val component = Node_Renderer_Component |
129 component.background = list.background |
|
130 component.foreground = list.foreground |
|
131 component.node_name = name |
128 component.node_name = name |
132 component.text = name.theory |
129 component.text = name.theory |
|
130 component |
133 } |
131 } |
134 } |
132 } |
135 status.renderer = new Node_Renderer |
133 status.renderer = new Node_Renderer |
136 |
134 |
137 private def handle_changed(changed_nodes: Set[Document.Node.Name]) |
135 private def handle_changed(changed_nodes: Set[Document.Node.Name]) |