phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

naming

Browse Source
This commit is contained in:
Jon Eugster
2023-06-19 16:26:24 +02:00
parent e67db092d5
commit 2fed94a2bb
2 changed files with 5 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/Level.tsx
+2 -2
View File
@@ -29,7 +29,7 @@ import { useStore } from 'react-redux';
import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts'; 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 { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection';
import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'; 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 type { Location } from 'vscode-languageserver-protocol';
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' 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 { // TODO: Is there any possibility that the editor connection takes a while
// and we should show a circular progress here? // and we should show a circular progress here?
commandLineMode && editorConnection && commandLineMode && editorConnection &&
<ReducedInterface world={worldId} level={levelId}/> <CommandLineInterface world={worldId} level={levelId}/>
} }
</div> </div>
</MonacoEditorContext.Provider> </MonacoEditorContext.Provider>
client/src/components/infoview/main.tsx
+3 -2
View File
@@ -22,7 +22,8 @@ import { levelCompleted, selectCompleted } from '../../state/progress';
import { GameIdContext } from '../../App'; import { GameIdContext } from '../../App';
import { InputModeContext } from '../Level'; 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}) { export function Main(props: {world: string, level: number}) {
const ec = React.useContext(EditorContext); const ec = React.useContext(EditorContext);
const gameId = React.useContext(GameIdContext) const gameId = React.useContext(GameIdContext)
@@ -116,7 +117,7 @@ export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, ed
</div> </div>
} }
export function ReducedInterface(props: {world: string, level: number}) { export function CommandLineInterface(props: {world: string, level: number}) {
const ec = React.useContext(EditorContext); const ec = React.useContext(EditorContext);
const gameId = React.useContext(GameIdContext) const gameId = React.useContext(GameIdContext)