diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx index 3ba79d22..e182bac6 100644 --- a/lean4-infoview/src/index.tsx +++ b/lean4-infoview/src/index.tsx @@ -7,7 +7,7 @@ export * from '@leanprover/infoview-api' export { EditorContext, EnvPosContext, VersionContext } from './infoview/contexts' export { EditorConnection } from './infoview/editorConnection' export { GoalLocation, GoalsLocation, LocationsContext } from './infoview/goalLocation' -export { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode' +export { InteractiveCode, InteractiveCodeProps, Markdown } from './infoview/interactiveCode' export { renderInfoview } from './infoview/main' export { RpcContext, useRpcSession } from './infoview/rpcSessions' export { ServerVersion } from './infoview/serverVersion' diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 91070a55..16f9a3c3 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -73,7 +73,7 @@ interface TypePopupContentsProps { * and then passes the content through to a Markdown renderer * (currently `remark`). */ -function Markdown({ contents }: { contents: string }): JSX.Element { +export function Markdown({ contents }: { contents: string }): JSX.Element { return (