()
| 290 | |
| 291 | // used to close files, stop servers etc. |
| 292 | public dispose(): void { |
| 293 | const children = [ |
| 294 | this.helpProvider, |
| 295 | this.aliasProvider, |
| 296 | this.packageManager, |
| 297 | this.treeViewWrapper, |
| 298 | ...this.helpPanels, |
| 299 | ...this.previewProviders |
| 300 | ]; |
| 301 | for (const child of children) { |
| 302 | if ( |
| 303 | child && |
| 304 | 'dispose' in child && |
| 305 | typeof child.dispose === 'function' |
| 306 | ) { |
| 307 | try { |
| 308 | child.dispose(); |
| 309 | } catch (e) {} |
| 310 | } |
| 311 | } |
| 312 | } |
| 313 | |
| 314 | // refresh cached help info |
| 315 | public async refresh(refreshTreeView: boolean = false): Promise<boolean> { |