add impressum

README.md

@@ -125,12 +125,19 @@ You can see installed lean toolchains with `elan toolchain list`
 and check the size of `~/.elan`.
 
 ### Legal information
-For legal purposes, we need to display contact details. When setting up your own server,
-you will need to modify the following files:
 
-- `client/src/config/text.tsx`: Update contact information & server location. (set them to
-  `null` if you don't need to display them in your country)
-- `client/public/index.html`: Update the `noscript` page with the correct contact details.
+Depending on the GDPR and laws applying to your server, you will need to provide the following
+information:
+
+- `client/config/config.tsx`, `serverCountry`: where your server is located.
+- `client/config/config.tsx`, `contactDetails`: used in privacy policy & impressum
+- `client/config/config.tsx`, `impressum`: further legal notes
+
+if `contactDetails` or `impressum` are not `null`, you will see an item `Impressum` in
+the dropdown menu containing that information.
+
+Further, you might need to add the impressum manually to `index.html`
+for people with javascript disabled!
 
 ## Development Instructions
 

client/src/Navigation.tsx

@@ -1,15 +1,16 @@
 import { ChangeEvent, Dispatch, FC, MouseEventHandler, ReactNode, SetStateAction, useContext, useState } from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { IconDefinition, faArrowRotateRight, faCode } from '@fortawesome/free-solid-svg-icons'
+import { IconDefinition, faArrowRotateRight, faCode, faInfo, faInfoCircle } from '@fortawesome/free-solid-svg-icons'
 import ZulipIcon from './assets/zulip.svg'
 import { faArrowUpRightFromSquare, faDownload, faBars, faXmark, faShield, faHammer, faGear, faStar, faUpload, faCloudArrowUp } from '@fortawesome/free-solid-svg-icons'
 import { saveAs } from 'file-saver'
 
 import SettingsPopup, { PreferencesContext } from './Popups/Settings'
-import PrivacyPopup from './Popups/PrivacyPolicy';
-import ToolsPopup from './Popups/Tools';
-import LoadUrlPopup from './Popups/LoadUrl';
-import LoadZulipPopup from './Popups/LoadZulip';
+import PrivacyPopup from './Popups/PrivacyPolicy'
+import ImpressumPopup from './Popups/Impressum'
+import ToolsPopup from './Popups/Tools'
+import LoadUrlPopup from './Popups/LoadUrl'
+import LoadZulipPopup from './Popups/LoadZulip'
 
 import lean4webConfig from './config/config'
 import './css/Modal.css'
@@ -153,6 +154,7 @@ export const Menu: FC <{
 
   // state for the popups
   const [privacyOpen, setPrivacyOpen] = useState(false)
+  const [impressumOpen, setImpressumOpen] = useState(false)
   const [toolsOpen, setToolsOpen] = useState(false)
   const [settingsOpen, setSettingsOpen] = useState(false)
 
@@ -212,15 +214,19 @@ export const Menu: FC <{
           setLoadZulipOpen={setLoadZulipOpen} />
       }
       <NavButton icon={faGear} text="Settings" onClick={() => {setSettingsOpen(true)}} />
-      <NavButton icon={faHammer} text="Lean Version Info" onClick={() => setToolsOpen(true)} />
+      <NavButton icon={faHammer} text="Lean Info" onClick={() => setToolsOpen(true)} />
       <NavButton icon={faArrowRotateRight} text="Restart server" onClick={restart} />
       <NavButton icon={faDownload} text="Save file" onClick={() => save(code)} />
       <NavButton icon={faShield} text={'Privacy policy'} onClick={() => {setPrivacyOpen(true)}} />
+      <NavButton icon={faInfoCircle} text={'Impressum'} onClick={() => {setImpressumOpen(true)}} />
       <NavButton icon={faArrowUpRightFromSquare} text="Lean community" href="https://leanprover-community.github.io/" />
       <NavButton icon={faArrowUpRightFromSquare} text="Lean documentation" href="https://leanprover.github.io/lean4/doc/" />
       <NavButton icon={faArrowUpRightFromSquare} text="GitHub" href="https://github.com/hhu-adam/lean4web" />
     </Dropdown>
     <PrivacyPopup open={privacyOpen} handleClose={() => setPrivacyOpen(false)} />
+    { (lean4webConfig.impressum || lean4webConfig.contactDetails) &&
+      <ImpressumPopup open={impressumOpen} handleClose={() => setImpressumOpen(false)} />
+    }
     <ToolsPopup open={toolsOpen} handleClose={() => setToolsOpen(false)} project={project} />
     <SettingsPopup open={settingsOpen} handleClose={() => setSettingsOpen(false)} closeNav={() => setOpenNav(false)}
       project={project} setProject={setProject} />

client/src/Popups/Impressum.tsx

@@ -0,0 +1,24 @@
+import { FC } from 'react'
+import { Popup } from '../Navigation'
+import lean4webConfig from '../config/config'
+
+/** The popup with the privacy policy. */
+const ImpressumPopup: FC<{
+  open: boolean
+  handleClose: () => void
+}> = ({open, handleClose}) => {
+  return <Popup open={open} handleClose={handleClose}>
+    <h2>Impressum</h2>
+
+    { lean4webConfig.contactDetails &&
+      <p>
+        <strong>Contact details</strong><br/>
+        {lean4webConfig.contactDetails}
+      </p>
+    }
+
+    { lean4webConfig.impressum }
+  </Popup>
+}
+
+export default ImpressumPopup

client/src/Popups/PrivacyPolicy.tsx

@@ -24,10 +24,10 @@ const PrivacyPopup: FC<{
       <p>Our server is located in {lean4webConfig.serverCountry}.</p>
     }
 
-    { lean4webConfig.contactInformation &&
+    { lean4webConfig.contactDetails &&
       <p>
-        <strong>Contact information:</strong><br/>
-        {lean4webConfig.contactInformation}
+        <strong>Contact details</strong><br/>
+        {lean4webConfig.contactDetails}
       </p>
     }
   </Popup>

client/src/config/config.tsx

@@ -1,4 +1,11 @@
-const lean4webConfig = {
+import { Project } from './docs' // look here for documentation of the individual config options
+
+const lean4webConfig : {
+  projects: Project[],
+  serverCountry: string | null
+  contactDetails: JSX.Element | null
+  impressum: JSX.Element | null
+} = {
   "projects": [
     { "folder": "mathlib-demo",
       "name": "Latest Mathlib",
@@ -19,16 +26,18 @@ const lean4webConfig = {
         { "file": "DuperDemo.lean",
           "name": "Duper" }]},
   ],
-  "serverCountry": "Germany",
-  "contactInformation": <>
-    Alexander Bentkamp,&nbsp;
-    <a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Jon Eugster</a><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 />
-  </>
+  "serverCountry": null,
+  // example:
+  // <>
+  //   <p>my name</p>
+  //   <p>my email</p>
+  // </>,
+  "contactDetails": null,
+  // example:
+  // <>
+  //   <p>our VAT number is ...</p>
+  // </>
+  "impressum": null
 }
 
 export default lean4webConfig

client/src/config/docs.tsx

@@ -0,0 +1,31 @@
+/**
+ * This file contains the documentation of the existing `config` options
+*/
+
+/** An example can be any Lean file which belongs to the project.
+ * The editor just reads the file content, but it makes sense for maintainability
+ * that you ensure the Lean project actually builds the file. */
+interface Example {
+  /** File to load; relative path in `lean4web/Projects/<projectfolder>/` */
+  file: string,
+  /** Display name used in the `Examples` menu */
+  name: string
+}
+
+/** You can add any Lean Project under `lean4web/Projects/` and add it here to use it in the
+ * web editor. Note that you will need to manually build your project. Alternatively
+ * you can add a file `lean4web/Projects/myProject/build.sh` which contains the instructions
+ * to update & build the project.
+ */
+interface Project {
+  /** The folder containing the Lean project; the folder is expected to be in `lean4web/Projects/`.
+   *  The folder name will appear in the URL.
+   */
+  folder: string,
+  /** Display name; shown in selection menu */
+  name: string,
+  /** A list of examples which are added under the menu `Examples` */
+  examples?: Example[]
+}
+
+export type { Example, Project }

index.html

@@ -8,17 +8,16 @@
   <body>
     <div id="root" class="monaco-workbench">
       <noscript>
-        <p>You need to enable JavaScript to use the lean4web editor, as it is a <a href="https://react.dev">React app</a>.</p>
-        <p>Contact details:</p>
         <p>
-          Alexander Bentkamp,&nbsp;
-          <a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Jon Eugster</a><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 />
+          You need to enable JavaScript to use the lean web editor,
+          as it is a <a href="https://react.dev">React app</a>.
         </p>
+        <!-- Manually providing contact details for the noscript site -->
+        <!-- <h2>Impressum</h2> -->
+        <!-- <strong>Contact details</strong> -->
+        <!-- <p> -->
+          <!-- your contact details -->
+        <!-- </p> -->
       </noscript>
     </div>
     <script type="module" src="/client/src/index.tsx"></script>