move Interfaces to infoview/main

client/src/components/Level.tsx

@@ -29,7 +29,7 @@ import { useStore } from 'react-redux';
 import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection';
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event';
-import { Main, EditorInterface } from './infoview/main'
+import { EditorInterface, ReducedInterface } from './infoview/main'
 import type { Location } from 'vscode-languageserver-protocol';
 
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
@@ -97,13 +97,6 @@ function ExerciseStatement({data}) {
   </Markdown></div>
 }
 
-function ReducedInterface({worldId, levelId, editorConnection}) {
-  return <div>
-    {/* <button className="btn" onClick={handleUndo} disabled={!canUndo}><FontAwesomeIcon icon={faRotateLeft} /> Undo</button> */}
-    {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
-  </div>
-}
-
 function PlayableLevel({worldId, levelId}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const chatPanelRef = useRef<HTMLDivElement>(null)
@@ -280,17 +273,16 @@ function PlayableLevel({worldId, levelId}) {
           <MonacoEditorContext.Provider value={editor}>
           <ExerciseStatement data={level?.data} />
           <div className="exercise">
-            {/* We need the editor to be hidden because the command line edits its content */}
+            {/* We need the editor to always there and hidden because
+              the command line edits its content */}
             <EditorInterface data={level?.data} codeviewRef={codeviewRef} hidden={commandLineMode}
                     worldId={worldId} levelId={levelId} editorConnection={editorConnection}/>
-            {commandLineMode && <ReducedInterface worldId={worldId} levelId={levelId} editorConnection={editorConnection}/>}
+            { // TODO: Is there any possibility that the editor connection takes a while
-            {/* <div className={`statement ${commandLineMode ? 'hidden' : ''}`}><code>{level?.data?.descrFormat}</code></div> */}
+              // and we should show a circular progress here?
-            {/* <div ref={codeviewRef} className={`codeview ${commandLineMode ? 'hidden' : ''}`}></div> */}
+              commandLineMode && editorConnection &&
+                <ReducedInterface world={worldId} level={levelId}/>
+            }
           </div>
-          {/* <div className="input-mode-switch">
-            {commandLineMode && <button className="btn" onClick={handleUndo} disabled={!canUndo}><FontAwesomeIcon icon={faRotateLeft} /> Undo</button>}
-          </div> */}
-                {/* {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />} */}
           </MonacoEditorContext.Provider>
           </EditorContext.Provider>
         </div>

client/src/components/infoview/main.tsx

@@ -115,3 +115,87 @@ export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, ed
 
   </div>
 }
+
+export function ReducedInterface(props: {world: string, level: number}) {
+
+  const ec = React.useContext(EditorContext);
+  const gameId = React.useContext(GameIdContext)
+
+  const dispatch = useAppDispatch()
+
+  // Mark level as completed when server gives notification
+  useServerNotificationEffect(
+      '$/game/completed',
+      (params: any) => {
+
+          if (ec.events.changedCursorLocation.current &&
+              ec.events.changedCursorLocation.current.uri === params.uri) {
+              dispatch(levelCompleted({game: gameId, world: props.world, level: props.level}))
+          }
+      },
+      []
+  );
+
+  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
+
+  /* Set up updates to the global infoview state on editor events. */
+  const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
+
+  const [allProgress, _1] = useServerNotificationState(
+      '$/lean/fileProgress',
+      new Map<DocumentUri, LeanFileProgressProcessingInfo[]>(),
+      async (params: LeanFileProgressParams) => (allProgress) => {
+          const newProgress = new Map(allProgress);
+          return newProgress.set(params.textDocument.uri, params.processing);
+      },
+      []
+  );
+
+  const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
+
+  useClientNotificationEffect(
+      'textDocument/didClose',
+      (params: DidCloseTextDocumentParams) => {
+          if (ec.events.changedCursorLocation.current &&
+              ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
+              ec.events.changedCursorLocation.fire(undefined)
+          }
+      },
+      []
+  );
+
+  const serverVersion =
+      useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
+  const serverStoppedResult = useEventResult(ec.events.serverStopped);
+  // NB: the cursor may temporarily become `undefined` when a file is closed. In this case
+  // it's important not to reconstruct the `WithBlah` wrappers below since they contain state
+  // that we want to persist.
+  let ret
+  if (!serverVersion) {
+      ret = <p>Waiting for Lean server to start...</p>
+  } else if (serverStoppedResult){
+      ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
+  } else {
+      ret = <div className="infoview vscode-light">
+          {completed && <div className="level-completed">Level completed! 🎉</div>}
+          <Infos />
+      </div>
+  }
+
+  return <div>
+    {/* <button className="btn" onClick={handleUndo} disabled={!canUndo}><FontAwesomeIcon icon={faRotateLeft} /> Undo</button> */}
+    <ConfigContext.Provider value={config}>
+      <VersionContext.Provider value={serverVersion}>
+        <WithRpcSessions>
+          <WithLspDiagnosticsContext>
+            <ProgressContext.Provider value={allProgress}>
+              {ret}
+            </ProgressContext.Provider>
+          </WithLspDiagnosticsContext>
+        </WithRpcSessions>
+      </VersionContext.Provider>
+    </ConfigContext.Provider>
+  </div>
+
+
+}