From 98ea870a43bf69943ccebf69725d4a191f94e429 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 1 Sep 2023 20:09:49 +0200
Subject: [PATCH] small fixes

---
 client/src/components/app_bar.tsx             |  6 +--
 .../src/components/infoview/command_line.tsx  |  6 +--
 client/src/components/infoview/main.tsx       | 16 +++---
 client/src/components/level.css               |  1 +
 client/src/components/level.tsx               |  7 ++-
 client/src/components/welcome.css             | 53 -------------------
 client/src/components/welcome.tsx             |  6 ++-
 client/src/components/world_tree.css          | 50 +++++++++++++++++
 client/src/components/world_tree.tsx          | 10 ++--
 9 files changed, 75 insertions(+), 80 deletions(-)

diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx
index c45b0b0..781489e 100644
--- a/client/src/components/app_bar.tsx
+++ b/client/src/components/app_bar.tsx
@@ -83,13 +83,11 @@ export function WelcomeAppBar({gameInfo, toggleImpressum, openEraseMenu, openUpl
         <Button inverted="false" title="back to games selection" to="/">
           <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
         </Button>
-        <span className="app-bar-title">
-          {}
-        </span>
+        <span className="app-bar-title"></span>
       </div>
       <div>
         <span className="app-bar-title">
-          {gameInfo?.title}
+          {mobile ? '' : gameInfo?.title}
         </span>
       </div>
       <div className="nav-btns">
diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx
index 100d54b..905c24b 100644
--- a/client/src/components/infoview/command_line.tsx
+++ b/client/src/components/infoview/command_line.tsx
@@ -64,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function CommandLine({proofPanelRef, hidden}: {proofPanelRef: React.MutableRefObject<HTMLDivElement>, hidden?: boolean}) {
+export function CommandLine({hidden}: {hidden?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -179,11 +179,9 @@ export function CommandLine({proofPanelRef, hidden}: {proofPanelRef: React.Mutab
         })
         // Save the proof to the context
         setProof(tmpProof)
-        console.debug('updated proof')
-        proofPanelRef.current?.lastElementChild?.scrollIntoView()
       })
     })
-  }, [editor, rpcSess, uri, model, proofPanelRef])
+  }, [editor, rpcSess, uri, model])
 
   // Run the command
   const runCommand = React.useCallback(() => {
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index f7a2437..2a6f32d 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -295,11 +295,6 @@ export function CommandLineInterface(props: { world: string, level: number, data
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
 
-  // React.useEffect(() => {
-  //   console.debug('updated proof')
-  //   // proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
-  // }, [proof])
-
   /** Delete all proof lines starting from a given line.
    * Note that the first line (i.e. deleting everything) is `1`!
    */
@@ -338,6 +333,11 @@ export function CommandLineInterface(props: { world: string, level: number, data
     }
   }
 
+  // Scroll to the end of the proof if it is updated.
+  React.useEffect(() => {
+    proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
+  }, [proof])
+
   // Scroll to element if selection changes
   React.useEffect(() => {
     if (typeof selectedStep !== 'undefined') {
@@ -412,13 +412,13 @@ export function CommandLineInterface(props: { world: string, level: number, data
   let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
   return <div className="commandline-interface">
-    <div className="content" ref={proofPanelRef}>
+    <div className="content">
       <div className="tmp-pusher">
         {!proof.length &&
           <CircularProgress />
         }
       </div>
-      <div className='proof'>
+      <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
         {proof.length ?
           <>
@@ -483,6 +483,6 @@ export function CommandLineInterface(props: { world: string, level: number, data
         }
       </div>
     </div>
-    <CommandLine proofPanelRef={proofPanelRef} hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
+    <CommandLine hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
   </div>
 }
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 862b1bf..fd6579f 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -26,6 +26,7 @@
 
 .inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
   height: 100%;
+  width: 100%;
   overflow: auto;
   position: relative;
 }
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 22c16ca..406f92f 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -392,10 +392,9 @@ function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
 
   return <div className="chat-panel">
     <div className="chat">
-      {text?.map((t =>
-        t.trim() ?
-          <Hint hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
-        : <></>
+      {text?.filter(t => t.trim()).map(((t, i) =>
+        <Hint key={`intro-p-${i}`}
+          hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
       {impressum ? <Impressum handleClose={closeImpressum} /> : null}
     </div>
diff --git a/client/src/components/welcome.css b/client/src/components/welcome.css
index 84fee15..94e17e3 100644
--- a/client/src/components/welcome.css
+++ b/client/src/components/welcome.css
@@ -58,59 +58,6 @@ h5, h6 {
   font-style: italic;
 }
 
-/***************/
-/* SVG Graphic */
-/***************/
-
-svg .world-title-wrapper, svg .level-title-wrapper div {
-  overflow: visible;
-}
-
-svg .world-title-wrapper div, svg .level-title-wrapper div {
-  width: 100%;
-  height: 100%;
-}
-
-svg .world-title-wrapper div, svg .level-title-wrapper div {
-  display: flex;
-  align-items:center;
-  justify-content:center;
-  overflow: visible;
-
-}
-
-svg .world-title, svg .level-title {
-  color: white;
-  margin: 0;
-  padding: 0;
-  text-align: center;
-}
-
-svg .world-title {
-  font-weight: 700;
-}
-
-svg .level-title {
-  font-weight: 400;
-  opacity: 0;
-  transition: opacity .3s;
-}
-
-svg .level:hover .level-title {
-  opacity: 1;
-}
-
-svg .disabled {
-  cursor: default;
-}
-
-.world-selection {
-  display: block;
-  margin-left: auto;
-  margin-right: auto;
-  margin-top: 2em;
-}
-
 /******************/
 /* Privacy Button */
 /******************/
diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx
index 36c6f29..1fd637e 100644
--- a/client/src/components/welcome.tsx
+++ b/client/src/components/welcome.tsx
@@ -35,9 +35,11 @@ function IntroductionPanel({introduction}: {introduction: string}) {
 
   return <div className="column chat-panel">
     <div className="chat">
-      {text?.map((t =>
+      {text?.map(((t, i) =>
         t.trim() ?
-          <Hint hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
+          <Hint key={`intro-p-${i}`}
+            hint={{text: t, hidden: false}}
+            step={0} selected={null} toggleSelection={undefined} />
         : <></>
       ))}
     </div>
diff --git a/client/src/components/world_tree.css b/client/src/components/world_tree.css
index a327076..f343eed 100644
--- a/client/src/components/world_tree.css
+++ b/client/src/components/world_tree.css
@@ -1,3 +1,53 @@
+svg .world-title-wrapper, svg .level-title-wrapper div {
+  overflow: visible;
+}
+
+svg .world-title-wrapper div, svg .level-title-wrapper div {
+  width: 100%;
+  height: 100%;
+}
+
+svg .world-title-wrapper div, svg .level-title-wrapper div {
+  display: flex;
+  align-items:center;
+  justify-content:center;
+  overflow: visible;
+
+}
+
+svg .world-title, svg .level-title {
+  color: white;
+  margin: 0;
+  padding: 0;
+  text-align: center;
+}
+
+svg .world-title {
+  font-weight: 700;
+}
+
+svg .level-title {
+  font-weight: 400;
+  opacity: 0;
+  transition: opacity .3s;
+}
+
+svg .level:hover .level-title {
+  opacity: 1;
+}
+
+svg .disabled {
+  cursor: default;
+}
+
+.world-selection {
+  display: block;
+  margin-left: auto;
+  margin-right: auto;
+  margin-top: 2em;
+  max-width: 100%;
+}
+
 .world-selection-menu {
   padding: .5em 1em;
   position: absolute;
diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx
index 3e54ed8..93043a9 100644
--- a/client/src/components/world_tree.tsx
+++ b/client/src/components/world_tree.tsx
@@ -268,7 +268,7 @@ export function WorldTreePanel({worlds, worldSize}:
     let elems = Array.from(document.getElementsByClassName("playable-world"))
     if (elems.length) {
       // it seems that the last element is the one furthest up in the tree
-      // TODO: I think they appear in random order. Check there position and select the lowest one
+      // TODO: I think they appear in random order. Check their position and select the lowest one
       // of these positions to scroll to.
       let elem = elems[0]
       console.debug(`scrolling to ${elem.textContent}`)
@@ -299,7 +299,8 @@ export function WorldTreePanel({worlds, worldSize}:
       // if the origin world is not completed, mark the target world as non-playable
       if (!sourceCompleted) {completed[edge[1]][0] = false}
       svgElements.push(
-        <WorldPath source={nodes[edge[0]]} target={nodes[edge[1]]} unlocked={sourceCompleted}/>
+        <WorldPath key={`path_${edge[0]}-->${edge[1]}`}
+          source={nodes[edge[0]]} target={nodes[edge[1]]} unlocked={sourceCompleted}/>
       )
     }
 
@@ -343,10 +344,9 @@ export function WorldTreePanel({worlds, worldSize}:
   return <div className="column">
       <WorldSelectionMenu />
       <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink"
-        width={bounds ? `${ds * dx}` : ''}
+          width={bounds ? `${ds * dx}` : ''}
           viewBox={bounds ? `${s*bounds.x1 - padding} ${s*bounds.y1 - padding} ${dx} ${s*(bounds.y2 - bounds.y1) + 2 * padding}` : ''}
-          className="world-selection"
-        >
+          className="world-selection" >
         {svgElements}
       </svg>
   </div>