diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index e1f64e0..c3830ee 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -22,7 +22,7 @@ import './level.css'
import { Button } from './Button'
import { ConnectionContext, useLeanClient } from '../connection';
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
-import { codeEdited, selectCode, progressSlice } from '../state/progress';
+import { codeEdited, selectCode, progressSlice, selectCompleted } from '../state/progress';
import { useAppDispatch, useAppSelector } from '../hooks';
import { useStore } from 'react-redux';
@@ -126,6 +126,7 @@ function Level() {
setCanUndo(code.trim() !== "")
}
+ const completed = useAppSelector(selectCompleted(worldId, levelId))
const {editor, infoProvider, editorConnection} =
useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
@@ -179,6 +180,8 @@ function Level() {
+
+ {completed &&
{level?.data?.conclusion}
}
{!level.isLoading && }
diff --git a/client/src/components/level.css b/client/src/components/level.css
index ba988dd..1674572 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -43,6 +43,10 @@
padding: 1em;
}
+.conclusion {
+ padding: 1em;
+}
+
.exercise {
flex: 1 1 auto;
display: flex;
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 713f4f8..d3f78cd 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -20,6 +20,7 @@ export interface ComputedInventoryItem {
interface LevelInfo {
title: null|string,
introduction: null|string,
+ conclusion: null|string,
index: number,
tactics: ComputedInventoryItem[],
lemmas: ComputedInventoryItem[],
diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean
index aab19bc..123269d 100644
--- a/server/leanserver/GameServer/Game.lean
+++ b/server/leanserver/GameServer/Game.lean
@@ -46,6 +46,7 @@ structure LevelInfo where
lemmas : Array ComputedInventoryItem
definitions : Array ComputedInventoryItem
introduction : String
+ conclusion : String
descrText : String := ""
descrFormat : String := ""
deriving ToJson, FromJson
@@ -125,7 +126,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
definitions := lvl.definitions.computed,
descrText := lvl.descrText,
descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
- introduction := lvl.introduction }
+ introduction := lvl.introduction
+ conclusion := lvl.conclusion }
c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
return true
| Message.request id "loadDoc" params =>