From 75f356f4b28288a4e3fbe9a7efe1141a1a43bdaf Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 6 Mar 2023 18:07:09 +0100
Subject: [PATCH] Add World introduction and change layout

---
 client/src/components/Level.tsx               | 60 ++++++++++++++++++-
 client/src/components/Welcome.tsx             |  2 +-
 client/src/components/infoview/info.tsx       |  6 +-
 client/src/components/infoview/infoview.css   |  4 ++
 client/src/components/level.css               | 19 +++---
 client/src/state/api.ts                       |  2 +-
 .../leanserver/GameServer/EnvExtensions.lean  |  5 +-
 7 files changed, 77 insertions(+), 21 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 0df2125..8adcc80 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -39,6 +39,7 @@ import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
 import Markdown from './Markdown';
 
 import Split from 'react-split'
+import { Alert } from '@mui/material';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(null as any);
 
@@ -129,7 +130,50 @@ function Level() {
   const completed = useAppSelector(selectCompleted(worldId, levelId))
 
   const {editor, infoProvider, editorConnection} =
-    useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
+  useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
+
+  // TODO: This is a hack for having an introduction (i.e. level 0)
+  // for each world.
+  if (levelId == 0) {
+    return <>
+      <div className="app-bar">
+        <div>
+        <Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button>
+          <span className="app-bar-title">
+          {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
+          </span>
+        </div>
+        <div>
+          <span className="app-bar-title">
+            {`Einführung`}
+          </span>
+          <Button disabled={levelId <= 1} inverted={true}
+            to={`/world/${worldId}/level/0`}
+            ><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
+          <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
+            to={`/world/${worldId}/level/1`}
+            >Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
+        </div>
+      </div>
+        <div className="exercise-panel">
+          <div ref={introductionPanelRef} className="introduction-panel">
+            <Alert severity="info" sx={{ mt: 1 }}>
+              <Markdown>
+                {gameInfo.data?.worlds.nodes[worldId].introduction}
+              </Markdown>
+            </Alert>
+          <div ref={codeviewRef} className={`codeview ${commandLineMode ? 'hidden' : ''}`}></div>
+        </div>
+        <div className="conclusion">
+          {levelId >= gameInfo.data?.worldSize[worldId] ?
+          <Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button> :
+          <Button to={`/world/${worldId}/level/1`}>
+            Start&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+          </Button>}
+        </div>
+      </div>
+    </>
+  }
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -144,7 +188,7 @@ function Level() {
         <span className="app-bar-title">
           {levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`}
         </span>
-        <Button disabled={levelId <= 1} inverted={true}
+        <Button disabled={levelId <= 0} inverted={true}
           to={`/world/${worldId}/level/${levelId - 1}`}
           ><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
         <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
@@ -153,13 +197,20 @@ function Level() {
       </div>
 
     </div>
-    <Split minSize={0} snapOffset={200} sizes={[30, 45, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
+    <Split minSize={0} snapOffset={200} sizes={[0, 50, 25, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
       <div className="side-panel">
+        {/*
         <div ref={introductionPanelRef} className="introduction-panel">
           <Markdown>{level?.data?.introduction}</Markdown>
         </div>
+        */}
       </div>
       <div className="exercise-panel">
+        <div ref={introductionPanelRef} className="introduction-panel">
+          <Alert severity="info" sx={{ mt: 1 }}>
+            <Markdown>{level?.data?.introduction}</Markdown>
+          </Alert>
+        </div>
         <div className="exercise">
           {/* <h4>Aufgabe:</h4> */}
           <Markdown>{level?.data?.descrText}</Markdown>
@@ -193,6 +244,9 @@ function Level() {
       <div className="doc-panel">
         {!level.isLoading && <Inventory tactics={level?.data?.tactics} lemmas={level?.data?.lemmas} definitions={level?.data?.definitions} />}
       </div>
+      <div className="side-panel">
+        <p>Display Tactic documentation here?</p>
+      </div>
     </Split>
   </>
 }
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index ced569d..1c97932 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -55,7 +55,7 @@ function Welcome() {
       let position: cytoscape.Position = nodes[id].position
 
       svgElements.push(
-        <Link key={`world${id}`} to={`/world/${id}/level/1`}>
+        <Link key={`world${id}`} to={`/world/${id}/level/0`}>
           <circle className="world-circle" cx={position.x} cy={position.y} r="8" />
           <text className="world-name"
             x={position.x} y={position.y}>{nodes[id].data.title ? nodes[id].data.title : id}</text>
diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx
index 6748bb8..85c6ba5 100644
--- a/client/src/components/infoview/info.tsx
+++ b/client/src/components/infoview/info.tsx
@@ -124,7 +124,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             <div className="goals-section">
                 { goals && (
                     goals.goals.length > 0
-                  ? <><div className="goals-section-title">Main Goal</div>
+                  ? <><div className="goals-section-title">Aktuelles Goal</div>
                     <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
                   : <div className="goals-section-title">No Goals</div>
                 ) }
@@ -148,8 +148,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 <><CircularProgress /><div>Loading goal...</div></>)}
         <AllMessages />
         <LocationsContext.Provider value={locs}>
-            {goals && goals.goals.length > 1 && <div className="goals-section">
-                    <div className="goals-section-title">Other Goals</div>
+            {goals && goals.goals.length > 1 && <div className="goals-section other-goals">
+                    <div className="goals-section-title">Weitere Goals</div>
 
                     {goals.goals.slice(1).map((goal, i) =>
                         <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal commandLine={false} filter={goalFilter} goal={goal} /></details>)}
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css
index 6a03114..650a679 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -75,3 +75,7 @@
 .command-line-input .monaco-editor .scroll-decoration {
   box-shadow: none;
 }
+
+.other-goals .goals-section-title, .other-goals summary, .other-goals summary .font-code {
+  color: #5191d1;
+}
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 1674572..b95cf9c 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -35,16 +35,15 @@
   background-color: #e9f2fb;
 }
 
-.infoview {
-  padding: 1em;
-}
-
-.exercise {
-  padding: 1em;
+.introduction-panel, .infoview, .exercise, .conclusion {
+  padding-top: 1em;
+  padding-left: 1em;
+  padding-right: 1em;
+  padding-bottom: 0;
 }
 
-.conclusion {
-  padding: 1em;
+.infoview {
+  padding-top: 0em;
 }
 
 .exercise {
@@ -64,10 +63,6 @@
   margin-bottom: 0;
 }
 
-.introduction-panel {
-  padding: 1em;
-}
-
 .input-mode-switch {
   margin: 0;
   display: flex;
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index d3f78cd..bd5268c 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -4,7 +4,7 @@ import { Connection } from '../connection'
 interface GameInfo {
   title: null|string,
   introduction: null|string,
-  worlds: null|{nodes: {[id:string]: {id: string, title: string}}, edges: string[][]},
+  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]},
   worldSize: null|{[key: string]: number},
   authors: null|string[],
   conclusion: null|string,
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 1d248a7..71500af 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -174,7 +174,10 @@ structure World where
 deriving Inhabited
 
 instance : ToJson World := ⟨
-  fun world => Json.mkObj [("name", toJson world.name), ("title", world.title)]
+  fun world => Json.mkObj [
+    ("name", toJson world.name),
+    ("title", world.title),
+    ("introduction", world.introduction)]
 ⟩
 
 /-! ## Game -/