doc-gen4
doc-gen4 copied to clipboard
Clicking links in the navbar or using the "Go to source" link produces an error in VS Code webviews
When embedding doc-gen4 in a VS Code webview and clicking links in an iframe, the webview does not navigate to the given location:
Unsafe attempt to initiate navigation for frame with URL 'https://leanprover-community.github.io/mathlib4_docs/index.html?vscodeBrowserReqId=1718796086963' from frame with URL 'https://leanprover-community.github.io/mathlib4_docs/navbar.html'. The frame attempting navigation is sandboxed, and is therefore disallowed from navigating its ancestors
This probably doesn't occur in the web browser because top windows use a relaxed policy regarding iframe navigation. It does however mean that we cannot properly embed doc-gen4 in the Lean 4 VS Code extension.