Feature: Show the dependency graph of the current file as an InfoView widget

[nileshtrivedi]

Lean4 supports custom User Widgets that are displayed in the InfoView.
ProofWidgets library uses this and makes it easy to render many visualizations, including graphs.

Here is an example, that shows the dependency graph of all constants appearing in a term:

It would be really useful to have an example script, or a #blueprint_graph command that shows the blueprint dependency graph of the current file in the InfoView panel, updating as the file changes.

[nileshtrivedi]

A bit hacky, but works :-)
Here is my full script.

[nileshtrivedi]

@hanwenzhu Any interest in implementing this feature properly? I used the LeanArchitect's JSON export functions to read the graph back. A cleaner approach would be to use LeanArchitech's core methods that return the dependency graph.