Tested on iterm2 as well. I am not able to view any widget. Sample code tested on:
module
public meta import ProofWidgets.Component.GraphDisplay
public meta import ProofWidgets.Component.HtmlDisplay
public meta import ProofWidgets.Component.InteractiveSvg
public meta section
/-! ## Directed graphs with `GraphDisplay` -/
open ProofWidgets Jsx
/-! ### Basic usage -/
def mkEdge (st : String × String) : GraphDisplay.Edge := {source := st.1, target := st.2}
-- Place your cursor here.
#html <GraphDisplay
vertices={#["a", "b", "c", "d", "e", "f"].map ({id := ·})}
edges={#[("b","c"), ("d","e"), ("e","f"), ("f","d")].map mkEdge}
/>
{
defaultEdgeAttrs = { { "fill", "var(--vscode-editor-foreground)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 2 }, { "markerEnd", "url(#arrow)" } },
edges = { {
attrs = {},
source = "b",
target = "c"
}, {
attrs = {},
source = "d",
target = "e"
}, {
attrs = {},
source = "e",
target = "f"
}, {
attrs = {},
source = "f",
target = "d"
} },
forces = { {
link = vim.empty_dict()
}, {
manyBody = vim.empty_dict()
}, {
x = vim.empty_dict()
}, {
y = vim.empty_dict()
} },
showDetails = false,
vertices = { {
boundingShape = {
circle = {
radius = 5
}
},
id = "a",
label = {
element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} }
}
}, {
boundingShape = {
circle = {
radius = 5
}
},
id = "b",
label = {
element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} }
}
}, {
boundingShape = {
circle = {
radius = 5
}
},
id = "c",
label = {
element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} }
}
}, {
boundingShape = {
circle = {
radius = 5
}
},
id = "d",
label = {
element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} }
}
}, {
boundingShape = {
circle = {
radius = 5
}
},
id = "e",
label = {
element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} }
}
}, {
boundingShape = {
circle = {
radius = 5
}
},
id = "f",
label = {
element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} }
}
} }
}
I tried toggling on the enable widget and checkhealth didn't indicate anything. Also installed resvg but also nothing. Above snippet works on vscode
Tested on iterm2 as well. I am not able to view any widget. Sample code tested on:
Output:
{ defaultEdgeAttrs = { { "fill", "var(--vscode-editor-foreground)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 2 }, { "markerEnd", "url(#arrow)" } }, edges = { { attrs = {}, source = "b", target = "c" }, { attrs = {}, source = "d", target = "e" }, { attrs = {}, source = "e", target = "f" }, { attrs = {}, source = "f", target = "d" } }, forces = { { link = vim.empty_dict() }, { manyBody = vim.empty_dict() }, { x = vim.empty_dict() }, { y = vim.empty_dict() } }, showDetails = false, vertices = { { boundingShape = { circle = { radius = 5 } }, id = "a", label = { element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} } } }, { boundingShape = { circle = { radius = 5 } }, id = "b", label = { element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} } } }, { boundingShape = { circle = { radius = 5 } }, id = "c", label = { element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} } } }, { boundingShape = { circle = { radius = 5 } }, id = "d", label = { element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} } } }, { boundingShape = { circle = { radius = 5 } }, id = "e", label = { element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} } } }, { boundingShape = { circle = { radius = 5 } }, id = "f", label = { element = { "circle", { { "r", 5 }, { "fill", "var(--vscode-editor-background)" }, { "stroke", "var(--vscode-editor-foreground)" }, { "strokeWidth", 1.5 } }, {} } } } } }I tried toggling on the enable widget and checkhealth didn't indicate anything. Also installed resvg but also nothing. Above snippet works on
vscode