94 var node_name = Document.Node.Name.empty |
94 var node_name = Document.Node.Name.empty |
95 override def paintComponent(gfx: Graphics2D) |
95 override def paintComponent(gfx: Graphics2D) |
96 { |
96 { |
97 nodes_status.get(node_name) match { |
97 nodes_status.get(node_name) match { |
98 case Some(st) if st.total > 0 => |
98 case Some(st) if st.total > 0 => |
99 val w = getWidth |
99 val size = peer.getSize() |
100 val h = getHeight |
100 val insets = border.getBorderInsets(this.peer) |
101 var end = w |
101 val w = size.width - insets.left - insets.right |
|
102 val h = size.height - insets.top - insets.bottom |
|
103 var end = size.width - insets.right |
102 for { |
104 for { |
103 (n, color) <- List( |
105 (n, color) <- List( |
104 (st.unprocessed, Isabelle_Markup.unprocessed1_color), |
106 (st.unprocessed, Isabelle_Markup.unprocessed1_color), |
105 (st.running, Isabelle_Markup.running_color), |
107 (st.running, Isabelle_Markup.running_color), |
106 (st.failed, Isabelle_Markup.error_color)) } |
108 (st.failed, Isabelle_Markup.error_color)) } |
107 { |
109 { |
108 gfx.setColor(color) |
110 gfx.setColor(color) |
109 val v = (n * w / st.total) max (if (n > 0) 2 else 0) |
111 val v = (n * w / st.total) max (if (n > 0) 2 else 0) |
110 gfx.fillRect(end - v, 0, v, h) |
112 gfx.fillRect(end - v, insets.top, v, h) |
111 end -= v |
113 end -= v |
112 } |
114 } |
113 case _ => |
115 case _ => |
114 } |
116 } |
115 super.paintComponent(gfx) |
117 super.paintComponent(gfx) |
122 { |
124 { |
123 def configure(list: ListView[_], isSelected: Boolean, focused: Boolean, |
125 def configure(list: ListView[_], isSelected: Boolean, focused: Boolean, |
124 name: Document.Node.Name, index: Int) |
126 name: Document.Node.Name, index: Int) |
125 { |
127 { |
126 component.opaque = false |
128 component.opaque = false |
|
129 component.background = list.background |
|
130 component.foreground = list.foreground |
127 component.node_name = name |
131 component.node_name = name |
128 component.text = name.theory |
132 component.text = name.theory |
129 } |
133 } |
130 } |
134 } |
131 status.renderer = new Node_Renderer |
135 status.renderer = new Node_Renderer |