lean_get_widgets
Retrieve panel widgets like proof visualizations and custom widgets at a specific cursor position in a Lean file. Useful for extracting detailed widget data for analysis.
Instructions
Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be large.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column number (1-indexed) | |
| file_path | Yes | Absolute path to Lean file |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| widgets | No | Widget instances (id, name, range, props) |