From cede6630dcd09da4d91b3ba1286c5be7aa50e63e Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 25 Nov 2022 13:49:12 +0100
Subject: [PATCH] show introduction

---
 client/src/components/Level.tsx        | 7 ++++++-
 server/leanserver/GameServer/Game.lean | 4 +++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index b4db328..02e4a32 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -4,6 +4,8 @@ import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
+import ReactMarkdown from 'react-markdown';
+import { MathJax } from "better-react-mathjax";
 
 import { Button } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
@@ -40,6 +42,7 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
   const [leanData, setLeanData] = useState({goals: []})
   const [history, setHistory] = useState([])
   const [lastTactic, setLastTactic] = useState("")
+  const [introduction, setIntroduction] = useState("")
   const [errors, setErrors] = useState([])
   const codeviewRef = useRef<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
@@ -109,6 +112,7 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
         setIndex(parseInt(res["index"]))
         setTacticDocs(res["tactics"])
         setLemmaDocs(res["lemmas"])
+        setIntroduction(res["introduction"])
         processResponse(res)
       });
 
@@ -156,13 +160,14 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
         <LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
       </Grid>
       <Grid xs={4}>
+        <MathJax><ReactMarkdown>{introduction}</ReactMarkdown></MathJax>
         <div ref={codeviewRef} className="codeview" style={{height: "20em"}}></div>
         {/* <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
           errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} /> */}
         <Message isOpen={messageOpen} content={message} close={closeMessage} />
       </Grid>
       <Grid xs={4}>
-        <div ref={infoviewRef} className="infoview"></div>
+        <div ref={infoviewRef} className="infoview vscode-light"></div>
         {index > 1 ? <Button onClick={() => { loadLevel(index - 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button> : null}
         {index < nbLevels ? <Button onClick={() => { loadLevel(index + 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button> : null}
         {/* <TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} /> */}
diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean
index 1a66795..e709859 100644
--- a/server/leanserver/GameServer/Game.lean
+++ b/server/leanserver/GameServer/Game.lean
@@ -28,6 +28,7 @@ structure LevelInfo where
   title : String
   tactics: Array TacticDocEntry
   lemmas: Array LemmaDocEntry
+  introduction : String
 deriving ToJson
 
 structure LoadLevelParams where
@@ -56,7 +57,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
           { index := lvl.index,
             title := lvl.title,
             tactics := lvl.tactics,
-            lemmas := lvl.lemmas }
+            lemmas := lvl.lemmas,
+            introduction := lvl.introduction }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
       return true
     | _ => return false