@leanprover/infoview
    Preparing search index...

    Function loadRenderInfoview

    • Dynamically load the infoview module, execute renderInfoview with the provided args, and pass its return value to next. See README.md for why this is needed.

      Parameters

      • imports: Record<string, string>

        is the imports section of an importmap. It must contain URLs for @leanprover/infoview, react, react/jsx-runtime, react-dom, It may include additional URLs. The listed libraries become importable from user widgets. Note that dist/ already includes these files, so the following works:

        {
        '@leanprover/infoview': 'https://unpkg.com/@leanprover/infoview/dist/index.production.min.js',
        'react': 'https://unpkg.com/@leanprover/infoview/dist/react.production.min.js',
        'react/jsx-runtime': 'https://unpkg.com/@leanprover/infoview/dist/react-jsx-runtime.production.min.js',
        'react-dom': 'https://unpkg.com/@leanprover/infoview/dist/react-dom.production.min.js',
        }
      • args: [editorApi: EditorApi, uiElement: HTMLElement]
      • next: (_: InfoviewApi) => void

      Returns void

    Settings
    Member Visibility