Skip to content

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

@mhuisi

Description

@mhuisi

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions