diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 061ae5f..fa39b04 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -20,7 +20,7 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { GameIdContext } from '../../app';
import { useAppDispatch, useAppSelector } from '../../hooks';
-import { LevelInfo } from '../../state/api';
+import { LevelInfo, useGetGameInfoQuery } from '../../state/api';
import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
import Markdown from '../markdown';
@@ -38,6 +38,8 @@ import { Hints, MoreHelpButton, filterHints } from '../hints';
import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
import { DiagnosticSeverity } from 'vscode-languageclient';
import { useTranslation } from 'react-i18next';
+import path from 'path';
+
/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
* always present, or the monaco editor cannot start.
@@ -260,6 +262,7 @@ const goalFilter = {
showLetValue: true
}
+// TODD: Mark for translation!
/** The display of a single entered lean command */
function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
// The first step will always have an empty command
@@ -274,8 +277,8 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
} else {
return