From 7a5229db56d75072317b9a2597bcb2b95328b55d Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 25 Aug 2024 14:25:45 +0200
Subject: [PATCH] update config docs

---
 client/src/config/config.tsx | 18 ++----------------
 client/src/config/docs.tsx   | 25 +++++++++++++++++++++----
 2 files changed, 23 insertions(+), 20 deletions(-)

diff --git a/client/src/config/config.tsx b/client/src/config/config.tsx
index 872cd31f..541ad515 100644
--- a/client/src/config/config.tsx
+++ b/client/src/config/config.tsx
@@ -1,11 +1,6 @@
-import { Project } from './docs' // look here for documentation of the individual config options
+import { LeanWebConfig } 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
-} = {
+const lean4webConfig : LeanWebConfig = {
   "projects": [
     { "folder": "mathlib-demo",
       "name": "Latest Mathlib",
@@ -27,16 +22,7 @@ const lean4webConfig : {
           "name": "Duper" }]},
   ],
   "serverCountry": null,
-  // example:
-  // <>
-  //   <p>my name</p>
-  //   <p>my email</p>
-  // </>,
   "contactDetails": null,
-  // example:
-  // <>
-  //   <p>our VAT number is ...</p>
-  // </>
   "impressum": null
 }
 
diff --git a/client/src/config/docs.tsx b/client/src/config/docs.tsx
index 5234dae1..e819bf26 100644
--- a/client/src/config/docs.tsx
+++ b/client/src/config/docs.tsx
@@ -5,7 +5,7 @@
 /** 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 {
+interface LeanWebExample {
   /** File to load; relative path in `lean4web/Projects/<projectfolder>/` */
   file: string,
   /** Display name used in the `Examples` menu */
@@ -17,7 +17,7 @@ interface Example {
  * you can add a file `lean4web/Projects/myProject/build.sh` which contains the instructions
  * to update & build the project.
  */
-interface Project {
+interface LeanWebProject {
   /** The folder containing the Lean project; the folder is expected to be in `lean4web/Projects/`.
    *  The folder name will appear in the URL.
    */
@@ -25,7 +25,24 @@ interface Project {
   /** Display name; shown in selection menu */
   name: string,
   /** A list of examples which are added under the menu `Examples` */
-  examples?: Example[]
+  examples?: LeanWebExample[]
 }
 
-export type { Example, Project }
+interface LeanWebConfig {
+  projects: LeanWebProject[],
+  /** Where the server is located. Use `null` to not display this information. */
+  serverCountry: string | null
+  /** Contact details of the server maintainer. Used in Privacy Policy and Impressum.
+   * Use `null` to not display this information.
+   * Note: This will be embedded inside a `<p>` tag! (example: `<>Hans Muster<br />hans@nowhere.com</>`)
+   */
+  contactDetails: JSX.Element | null
+  /** Additional legal information shown in impressum alongside the contact details.
+   * Use `null` to not display this information.
+   * (example: `<><p>vat number: 000</p><>`)
+   */
+  impressum: JSX.Element | null
+
+}
+
+export type { LeanWebExample, LeanWebProject, LeanWebConfig }