Open mhuisi opened 2 months ago
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.
When embedding doc-gen4 in a VS Code webview and clicking links in an iframe, the webview does not navigate to the given location:
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.