From 2fed94a2bb1001e970b347d47da7c928b3e59ec1 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 19 Jun 2023 16:26:24 +0200
Subject: [PATCH] naming

---
 client/src/components/Level.tsx         | 4 ++--
 client/src/components/infoview/main.tsx | 5 +++--
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 4908a9f..d8e02d4 100644
--- a/client/src/components/Level.tsx
+++ b/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 { EditorInterface, ReducedInterface } from './infoview/main'
+import { EditorInterface, CommandLineInterface } from './infoview/main'
 import type { Location } from 'vscode-languageserver-protocol';
 
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
@@ -280,7 +280,7 @@ function PlayableLevel({worldId, levelId}) {
             { // TODO: Is there any possibility that the editor connection takes a while
               // and we should show a circular progress here?
               commandLineMode && editorConnection &&
-                <ReducedInterface world={worldId} level={levelId}/>
+                <CommandLineInterface world={worldId} level={levelId}/>
             }
           </div>
           </MonacoEditorContext.Provider>
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 5ffa88a..5c151ed 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -22,7 +22,8 @@ import { levelCompleted, selectCompleted } from '../../state/progress';
 import { GameIdContext } from '../../App';
 import { InputModeContext } from '../Level';
 
-
+// TODO: This is only used in `EditorInterface`
+// while `CommandLineInterface` has this copy-pasted in.
 export function Main(props: {world: string, level: number}) {
     const ec = React.useContext(EditorContext);
     const gameId = React.useContext(GameIdContext)
@@ -116,7 +117,7 @@ export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, ed
   </div>
 }
 
-export function ReducedInterface(props: {world: string, level: number}) {
+export function CommandLineInterface(props: {world: string, level: number}) {
 
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)