feat: export Markdown component

leanprover · Oct 16, 2024 · b135ee3 · b135ee3
1 parent f65cf74
commit b135ee3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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 (
         <ReactMarkdown
             children={contents}