From 64a1a3e5d333bbbea4a99b38aea374b59483e062 Mon Sep 17 00:00:00 2001
From: Alissa Tung <alissa-tung@outlook.com>
Date: Sun, 17 Dec 2023 02:09:25 +0800
Subject: [PATCH] refactor: split `renderInfoview`

---
 lean4-infoview/src/index.tsx         |  2 +-
 lean4-infoview/src/infoview/main.tsx | 30 +++++++++++++++++++++-------
 2 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx
index 01361452a..8297c24ab 100644
--- a/lean4-infoview/src/index.tsx
+++ b/lean4-infoview/src/index.tsx
@@ -17,7 +17,7 @@ export { importWidgetModule, DynamicComponent, DynamicComponentProps,
     PanelWidgetProps } from './infoview/userWidget';
 
 export { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode';
-export { renderInfoview } from './infoview/main';
+export { renderInfoview, mkInfoviewApi, Infoview } from './infoview/main';
 
 export { MessageData };
 
diff --git a/lean4-infoview/src/infoview/main.tsx b/lean4-infoview/src/infoview/main.tsx
index 3d89f7685..8a6987913 100644
--- a/lean4-infoview/src/infoview/main.tsx
+++ b/lean4-infoview/src/infoview/main.tsx
@@ -91,6 +91,12 @@ function Main(props: {}) {
   * @returns a collection of methods which must be invoked when the relevant editor events occur.
   */
 export function renderInfoview(editorApi: EditorApi, uiElement: HTMLElement): InfoviewApi {
+    const [editorEvents, infoviewApi] = mkInfoviewApi();
+    connInfoview(editorApi, editorEvents, uiElement);
+    return infoviewApi;
+}
+
+export const mkInfoviewApi = (): [EditorEvents, InfoviewApi] => {
     const editorEvents: EditorEvents = {
         initialize: new EventEmitter(),
         gotServerNotification: new EventEmitter(),
@@ -125,16 +131,26 @@ export function renderInfoview(editorApi: EditorApi, uiElement: HTMLElement): In
         getInfoviewHtml: async () => document.body.innerHTML,
     };
 
-    const ec = new EditorConnection(editorApi, editorEvents);
+    return [editorEvents, infoviewApi]
+}
 
-    editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc))
+export const Infoview:
+    React.FC<{ editorApi: EditorApi, editorEvents: EditorEvents }> =
+    ({ editorApi, editorEvents }) => {
+        const ecRef = React.useRef(new EditorConnection(editorApi, editorEvents));
+        const ec = ecRef.current;
+        React.useEffect(() => {
+            editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc))
+        }, [])
+
+        return (<EditorContext.Provider value={ec}>
+            <Main />
+        </EditorContext.Provider>)
+    }
 
+const connInfoview = (editorApi: EditorApi, editorEvents: EditorEvents, uiElement: HTMLElement) => {
     const root = ReactDOM.createRoot(uiElement)
     root.render(<React.StrictMode>
-        <EditorContext.Provider value={ec}>
-            <Main/>
-        </EditorContext.Provider>
+        <Infoview editorApi={editorApi} editorEvents={editorEvents} ></Infoview>
     </React.StrictMode>)
-
-    return infoviewApi;
 }