doc-gen4 icon indicating copy to clipboard operation
doc-gen4 copied to clipboard

Clicking links in the navbar or using the "Go to source" link produces an error in VS Code webviews

Open mhuisi opened this issue 8 months ago • 0 comments

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.

mhuisi avatar Jun 19 '24 11:06 mhuisi