48 size = new_size |
48 size = new_size |
49 } |
49 } |
50 } |
50 } |
51 } |
51 } |
52 |
52 |
53 private object Node_Renderer_Component extends BorderPanel { |
|
54 opaque = true |
|
55 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
|
56 |
|
57 var node_name: Document.Node.Name = Document.Node.Name.empty |
|
58 |
|
59 val required_geometry = new Geometry |
|
60 val required = new CheckBox { |
|
61 opaque = false |
|
62 override def paintComponent(gfx: Graphics2D): Unit = { |
|
63 super.paintComponent(gfx) |
|
64 required_geometry.update(location, size) |
|
65 } |
|
66 } |
|
67 |
|
68 val label_geometry = new Geometry |
|
69 val label: Label = new Label { |
|
70 background = view.getTextArea.getPainter.getBackground |
|
71 foreground = view.getTextArea.getPainter.getForeground |
|
72 opaque = false |
|
73 xAlignment = Alignment.Leading |
|
74 |
|
75 override def paintComponent(gfx: Graphics2D): Unit = { |
|
76 def paint_segment(x: Int, w: Int, color: Color): Unit = { |
|
77 gfx.setColor(color) |
|
78 gfx.fillRect(x, 0, w, size.height) |
|
79 } |
|
80 |
|
81 paint_segment(0, size.width, background) |
|
82 nodes_status.get(node_name) match { |
|
83 case Some(node_status) => |
|
84 val segments = |
|
85 List( |
|
86 (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), |
|
87 (node_status.running, PIDE.options.color_value("running_color")), |
|
88 (node_status.warned, PIDE.options.color_value("warning_color")), |
|
89 (node_status.failed, PIDE.options.color_value("error_color")) |
|
90 ).filter(_._1 > 0) |
|
91 |
|
92 segments.foldLeft(size.width - 2) { |
|
93 case (last, (n, color)) => |
|
94 val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 |
|
95 paint_segment(last - w, w, color) |
|
96 last - w - 1 |
|
97 } |
|
98 |
|
99 case None => |
|
100 paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) |
|
101 } |
|
102 super.paintComponent(gfx) |
|
103 |
|
104 label_geometry.update(location, size) |
|
105 } |
|
106 } |
|
107 |
|
108 def label_border(name: Document.Node.Name): Unit = { |
|
109 val st = nodes_status.overall_node_status(name) |
|
110 val color = |
|
111 st match { |
|
112 case Document_Status.Overall_Node_Status.ok => |
|
113 PIDE.options.color_value("ok_color") |
|
114 case Document_Status.Overall_Node_Status.failed => |
|
115 PIDE.options.color_value("failed_color") |
|
116 case _ => label.foreground |
|
117 } |
|
118 val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3 |
|
119 val thickness2 = 4 - thickness1 |
|
120 |
|
121 label.border = |
|
122 BorderFactory.createCompoundBorder( |
|
123 BorderFactory.createLineBorder(color, thickness1), |
|
124 BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) |
|
125 } |
|
126 |
|
127 layout(required) = BorderPanel.Position.West |
|
128 layout(label) = BorderPanel.Position.Center |
|
129 } |
|
130 |
|
131 private def in_required(location0: Point, p: Point): Boolean = |
|
132 Node_Renderer_Component != null && Node_Renderer_Component.required_geometry.in(location0, p) |
|
133 |
|
134 private def in_label(location0: Point, p: Point): Boolean = |
|
135 Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p) |
|
136 |
|
137 private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { |
53 private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { |
|
54 private object component extends BorderPanel { |
|
55 opaque = true |
|
56 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
|
57 |
|
58 var node_name: Document.Node.Name = Document.Node.Name.empty |
|
59 |
|
60 val required_geometry = new Geometry |
|
61 val required = new CheckBox { |
|
62 opaque = false |
|
63 override def paintComponent(gfx: Graphics2D): Unit = { |
|
64 super.paintComponent(gfx) |
|
65 required_geometry.update(location, size) |
|
66 } |
|
67 } |
|
68 |
|
69 val label_geometry = new Geometry |
|
70 val label: Label = new Label { |
|
71 background = view.getTextArea.getPainter.getBackground |
|
72 foreground = view.getTextArea.getPainter.getForeground |
|
73 opaque = false |
|
74 xAlignment = Alignment.Leading |
|
75 |
|
76 override def paintComponent(gfx: Graphics2D): Unit = { |
|
77 def paint_segment(x: Int, w: Int, color: Color): Unit = { |
|
78 gfx.setColor(color) |
|
79 gfx.fillRect(x, 0, w, size.height) |
|
80 } |
|
81 |
|
82 paint_segment(0, size.width, background) |
|
83 nodes_status.get(node_name) match { |
|
84 case Some(node_status) => |
|
85 val segments = |
|
86 List( |
|
87 (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), |
|
88 (node_status.running, PIDE.options.color_value("running_color")), |
|
89 (node_status.warned, PIDE.options.color_value("warning_color")), |
|
90 (node_status.failed, PIDE.options.color_value("error_color")) |
|
91 ).filter(_._1 > 0) |
|
92 |
|
93 segments.foldLeft(size.width - 2) { |
|
94 case (last, (n, color)) => |
|
95 val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 |
|
96 paint_segment(last - w, w, color) |
|
97 last - w - 1 |
|
98 } |
|
99 |
|
100 case None => |
|
101 paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) |
|
102 } |
|
103 super.paintComponent(gfx) |
|
104 |
|
105 label_geometry.update(location, size) |
|
106 } |
|
107 } |
|
108 |
|
109 def label_border(name: Document.Node.Name): Unit = { |
|
110 val st = nodes_status.overall_node_status(name) |
|
111 val color = |
|
112 st match { |
|
113 case Document_Status.Overall_Node_Status.ok => |
|
114 PIDE.options.color_value("ok_color") |
|
115 case Document_Status.Overall_Node_Status.failed => |
|
116 PIDE.options.color_value("failed_color") |
|
117 case _ => label.foreground |
|
118 } |
|
119 val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3 |
|
120 val thickness2 = 4 - thickness1 |
|
121 |
|
122 label.border = |
|
123 BorderFactory.createCompoundBorder( |
|
124 BorderFactory.createLineBorder(color, thickness1), |
|
125 BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) |
|
126 } |
|
127 |
|
128 layout(required) = BorderPanel.Position.West |
|
129 layout(label) = BorderPanel.Position.Center |
|
130 } |
|
131 |
|
132 def in_required(location0: Point, p: Point): Boolean = |
|
133 component.required_geometry.in(location0, p) |
|
134 |
|
135 def in_label(location0: Point, p: Point): Boolean = |
|
136 component.label_geometry.in(location0, p) |
|
137 |
138 def componentFor( |
138 def componentFor( |
139 list: ListView[_ <: isabelle.Document.Node.Name], |
139 list: ListView[_ <: isabelle.Document.Node.Name], |
140 isSelected: Boolean, |
140 isSelected: Boolean, |
141 focused: Boolean, |
141 focused: Boolean, |
142 name: Document.Node.Name, |
142 name: Document.Node.Name, |
143 index: Int |
143 index: Int |
144 ): Component = { |
144 ): Component = { |
145 val component = Node_Renderer_Component |
|
146 component.node_name = name |
145 component.node_name = name |
147 component.required.selected = |
146 component.required.selected = |
148 (if (document) document_required else theory_required).contains(name) |
147 (if (document) document_required else theory_required).contains(name) |
149 component.label_border(name) |
148 component.label_border(name) |
150 component.label.text = name.theory_base_name |
149 component.label.text = name.theory_base_name |
167 reactions += { |
168 reactions += { |
168 case MouseClicked(_, point, _, clicks, _) => |
169 case MouseClicked(_, point, _, clicks, _) => |
169 val index = peer.locationToIndex(point) |
170 val index = peer.locationToIndex(point) |
170 if (index >= 0) { |
171 if (index >= 0) { |
171 val index_location = peer.indexToLocation(index) |
172 val index_location = peer.indexToLocation(index) |
172 if (in_required(index_location, point)) { |
173 if (node_renderer.in_required(index_location, point)) { |
173 if (clicks == 1) { |
174 if (clicks == 1) { |
174 Document_Model.node_required(listData(index), toggle = true, document = document) |
175 Document_Model.node_required(listData(index), toggle = true, document = document) |
175 } |
176 } |
176 } |
177 } |
177 else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) |
178 else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) |
178 } |
179 } |
179 case MouseMoved(_, point, _) => |
180 case MouseMoved(_, point, _) => |
180 val index = peer.locationToIndex(point) |
181 val index = peer.locationToIndex(point) |
181 val index_location = peer.indexToLocation(index) |
182 val index_location = peer.indexToLocation(index) |
182 if (index >= 0 && in_required(index_location, point)) { |
183 if (index >= 0 && node_renderer.in_required(index_location, point)) { |
183 tooltip = |
184 tooltip = |
184 if (document) "Mark for inclusion in document" |
185 if (document) "Mark for inclusion in document" |
185 else "Mark as required for continuous checking" |
186 else "Mark as required for continuous checking" |
186 } |
187 } |
187 else if (index >= 0 && in_label(index_location, point)) { |
188 else if (index >= 0 && node_renderer.in_label(index_location, point)) { |
188 val name = listData(index) |
189 val name = listData(index) |
189 val st = nodes_status.overall_node_status(name) |
190 val st = nodes_status.overall_node_status(name) |
190 tooltip = |
191 tooltip = |
191 "theory " + quote(name.theory) + |
192 "theory " + quote(name.theory) + |
192 (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") |
193 (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") |