Skip to content

Commit

Permalink
update config docs
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Aug 25, 2024
1 parent 8815759 commit 7a5229d
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 20 deletions.
18 changes: 2 additions & 16 deletions client/src/config/config.tsx
Original file line number Diff line number Diff line change
@@ -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",
Expand All @@ -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
}

Expand Down
25 changes: 21 additions & 4 deletions client/src/config/docs.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand All @@ -17,15 +17,32 @@ 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.
*/
folder: string,
/** 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 />[email protected]</>`)
*/
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 }

0 comments on commit 7a5229d

Please sign in to comment.