add impressum

client/src/app.css

@@ -106,7 +106,8 @@ em {
   flex-direction: row;
   justify-content: space-between;
   padding: 1.1em;
-  filter: drop-shadow(0 0 5px rgba(0,0,0,0.5))
+  filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
+  z-index: 2;
 }
 
 .app-bar-title, .app-bar-subtitle {

client/src/components/level.css

@@ -24,9 +24,10 @@
   background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg==');
 }
 
-.inventory-panel, .exercise-panel, .doc-panel {
+.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
   height: 100%;
   overflow: auto;
+  position: relative;
 }
 
 .infoview {
@@ -258,3 +259,13 @@ td code  {
   margin-left: auto;
   margin-right: auto;
 }
+
+.impressum {
+  background-color: #fff;
+  width: 100%;
+  height: 100%;
+  position: absolute;
+  top: 0;
+  z-index: 1;
+  padding: .5rem;
+}

client/src/components/level.tsx

@@ -26,7 +26,7 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event';
 import type { Location } from 'vscode-languageserver-protocol';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
+import { faHome, faCircleInfo, faArrowRight, faArrowLeft, faShield, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
 import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
 
 import { GameIdContext } from '../app';
@@ -42,6 +42,7 @@ import { DeletedHint, DeletedHints, Hints } from './hints';
 import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './infoview/context';
 import { hasInteractiveErrors } from './infoview/command_line';
 import { GameHint } from './infoview/rpc_api';
+import { Impressum } from './privacy_policy';
 
 function Level() {
 
@@ -88,6 +89,16 @@ function PlayableLevel({worldId, levelId}) {
 
   const theme = useTheme();
 
+  const [impressum, setImpressum] = React.useState(false)
+
+  function closeImpressum() {
+    setImpressum(false)
+  }
+
+  function toggleImpressum() {
+    setImpressum(!impressum)
+  }
+
   useEffect(() => {
     // // Scroll to top when loading a new level
     // // TODO: Thats the wrong behaviour probably
@@ -250,7 +261,7 @@ function PlayableLevel({worldId, levelId}) {
     <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
     <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
     <ProofContext.Provider value={{proof, setProof}}>
-      <LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
+      <LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} toggleImpressum={toggleImpressum}/>
       <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
         <div className="chat-panel">
           <div ref={chatRef} className="chat">
@@ -316,6 +327,7 @@ function PlayableLevel({worldId, levelId}) {
               </div>
             </MonacoEditorContext.Provider>
           </EditorContext.Provider>
+          {impressum ? <Impressum handleClose={closeImpressum} /> : null}
         </div>
         <div className="inventory-panel">
           {!level.isLoading &&
@@ -341,13 +353,26 @@ function Introduction({worldId}) {
   const gameId = React.useContext(GameIdContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
+  const [impressum, setImpressum] = React.useState(false)
+
+  const closeImpressum = () => {
+    setImpressum(false)
+  }
+
+  const toggleImpressum = () => {
+    setImpressum(!impressum)
+  }
+
   return <>
     <div style={gameInfo.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
-    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" worldId={worldId} levelId={0} />
+    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" worldId={worldId} levelId={0} toggleImpressum={toggleImpressum}/>
     <div style={gameInfo.isLoading ? {display: "none"} : null} className="introduction-panel">
+      <div className="content-wrapper">
         <Markdown>
           {gameInfo.data?.worlds.nodes[worldId].introduction}
         </Markdown>
+        {impressum ? <Impressum handleClose={closeImpressum} /> : null}
+      </div>
       {gameInfo.data?.worldSize[worldId] == 0 ?
         <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
         <Button to={`/${gameId}/world/${worldId}/level/1`}>
@@ -358,7 +383,8 @@ function Introduction({worldId}) {
   </>
 }
 
-function LevelAppBar({isLoading, levelId, worldId, levelTitle}) {
+/** The top-navigation bar */
+function LevelAppBar({isLoading, levelId, worldId, levelTitle, toggleImpressum}) {
   const gameId = React.useContext(GameIdContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
@@ -375,14 +401,18 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) {
       <span className="app-bar-title">
         {levelTitle}
       </span>
-        <Button disabled={levelId <= 0} inverted="true" to=""
+        <Button disabled={levelId <= 0} inverted="true" to="" onClick={(ev) => { setCommandLineMode(!commandLineMode) }}>
-          onClick={(ev) => { setCommandLineMode(!commandLineMode) }}>Editor</Button>
+          Editor
-      <Button disabled={levelId <= 0} inverted="true"
+        </Button>
-        to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
+        <Button disabled={levelId <= 0} inverted="true" to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}>
-        ><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
+          <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-      <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted="true"
+        </Button>
-        to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}
+        <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted="true" to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
-        >Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
+          Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+        </Button>
+        <Button title="Information, Impressum, Privacy Policy" inverted="true" to="" onClick={toggleImpressum}>
+          <FontAwesomeIcon icon={faCircleInfo} />
+        </Button>
     </div>
 
   </div>

client/src/components/privacy_policy.tsx

@@ -10,7 +10,7 @@ import * as React from 'react'
  * `handleClose` is the function to close it again because it's open/closed state is
  * controlled by the containing element.
  */
-function PrivacyPolicyPopup (handleClose) {
+export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
   return <div className="modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
@@ -43,7 +43,7 @@ function PrivacyPolicyPopup (handleClose) {
 </div>
 }
 
-const PrivacyPolicy: React.FC = () => {
+export const PrivacyPolicy: React.FC = () => {
   const [open, setOpen] = React.useState(false)
   const handleOpen = () => setOpen(true)
   const handleClose = () => setOpen(false)
@@ -59,4 +59,48 @@ const PrivacyPolicy: React.FC = () => {
   )
 }
 
-export {PrivacyPolicy, PrivacyPolicyPopup}
+export function Impressum({handleClose}) {
+  return <div className="impressum">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Funding</h2>
+    <p>
+      This Lean game engine has been developed as part of the
+      project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
+      Age of Mathematics</a> at
+      Heinrich-Heine-Universität Düsseldorf. It is funded by
+      the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
+    </p>
+
+    <h2>Development</h2>
+    <p>
+      The source code is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
+      If you experience any problems, please
+      file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
+      get directly in contact.
+    </p>
+    <h2>Privacy Policy &amp; Impressum</h2>
+    <p>
+      Our server collects metadata (such as IP address, browser, operating system)
+      and the data that the user enters into the editor. The data is used to
+      compute the Lean output and display it to the user. The information will be stored
+      as long as the user stays on our website and will be deleted immediately afterwards.
+      We keep logs to improve our software, but the contained data is anonymised.
+    </p>
+    <p>
+      We do not use cookies, but your game progress is stored in the browser storage
+      as site data. Your game progress is not saved on the server; if you delete
+      your browser storage, it is completely gone.
+    </p>
+    <p>Our server is located in Germany.</p>
+    <p>
+      <strong>Contact information:</strong><br />
+      Jon Eugster<br />
+      Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
+      Universitätsstr. 1<br />
+      40225 Düsseldorf<br />
+      Germany<br />
+      +49 211 81-12173<br />
+      <a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
+    </p>
+  </div>
+}