hide hidden projects

Author: joneugster

client/src/config/config.ts client/config.tsclient/src/config/config.ts renamed to client/config.ts

@@ -1,7 +1,7 @@
-import type { LeanWebConfig } from './types'
+import { LeanWebConfig } from "./src/api/config-types";
 
 export const lean4webConfig: LeanWebConfig = {
   serverCountry: null,
   contactDetails: null,
   impressum: null,
-}
+};

client/src/App.tsx

@@ -17,7 +17,7 @@ import { Menu } from './navigation/Navigation'
 import { mobileAtom, settingsAtom } from './settings/settings-atoms'
 import { lightThemes } from './settings/settings-types'
 import { freshlyImportedCodeAtom } from './store/import-atoms'
-import { projectAtom } from './store/project-atoms'
+import { currentProjectAtom } from './store/project-atoms'
 import { screenWidthAtom } from './store/window-atoms'
 import { save } from './utils/SaveToFile'
 
@@ -35,7 +35,7 @@ function App() {
   const [settings] = useAtom(settingsAtom)
   const [mobile] = useAtom(mobileAtom)
   const [, setScreenWidth] = useAtom(screenWidthAtom)
-  const [project] = useAtom(projectAtom)
+  const [project] = useAtom(currentProjectAtom)
   const [code, setCode] = useAtom(codeAtom)
   const [freshlyImportedCode] = useAtom(freshlyImportedCodeAtom)
 
@@ -76,7 +76,7 @@ function App() {
       (window.location.protocol === 'https:' ? 'wss://' : 'ws://') +
       window.location.host +
       '/websocket/' +
-      project
+      project.folder
     console.log(`[Lean4web] Socket url is ${socketUrl}`)
     var _options: LeanMonacoOptions = {
       websocket: { url: socketUrl },
@@ -108,7 +108,7 @@ function App() {
 
   // Setting up the editor and infoview
   useEffect(() => {
-    if (project === undefined) return
+    if (!project) return
     console.debug('[Lean4web] Restarting editor')
     var _leanMonaco = new LeanMonaco()
     var leanMonacoEditor = new LeanMonacoEditor()
@@ -118,7 +118,7 @@ function App() {
       await _leanMonaco.start(options)
       await leanMonacoEditor.start(
         editorRef.current!,
-        path.join(project, `${project}.lean`),
+        path.join(project.folder, `${project.folder}.lean`),
         code ?? '',
       )
 

client/src/Popups/Impressum.tsx

@@ -1,4 +1,4 @@
-import { lean4webConfig } from '../config/config'
+import { lean4webConfig } from '../../config'
 import { Popup } from '../navigation/Popup'
 
 /** The popup with the privacy policy. */

client/src/Popups/PrivacyPolicy.tsx

@@ -1,4 +1,4 @@
-import { lean4webConfig } from '../config/config'
+import { lean4webConfig } from '../../config'
 import { Popup } from '../navigation/Popup'
 
 /** The popup with the privacy policy. */

client/src/api/config-types.ts

@@ -0,0 +1,16 @@
+import { JSX } from 'react'
+
+export type LeanWebConfig = {
+  /** 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
+}

client/src/api/project-types.ts

@@ -0,0 +1,28 @@
+/** 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. */
+export type LeanWebExample = {
+  /** File to load; relative path in `lean4web/Projects/<project_folder>/` */
+  file: string
+  /** Display name used in the `Examples` menu */
+  name: string
+}
+
+/** Configuration from a project's `leanweb-config.json` file. */
+export type LeanWebProjectConfig = {
+  /** Display name; shown in selection menu */
+  name: string
+  /** Hidden projects do not appear in the dropdown and are only accessible through the direct link */
+  hidden: boolean
+  /** The default project. There must be exactly one project marked as default */
+  default: boolean
+  /** A list of examples which are added under the menu `Examples` */
+  examples: LeanWebExample[]
+}
+
+/* A project */
+export type LeanWebProject = {
+  /* The folder name of the project. */
+  folder: string
+  config: LeanWebProjectConfig
+}

client/src/config/types.ts

@@ -18,8 +18,8 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { useAtom } from 'jotai'
 import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react'
 
+import { lean4webConfig } from '../../config'
 import ZulipIcon from '../assets/zulip.svg'
-import { lean4webConfig } from '../config/config'
 import { codeAtom } from '../editor/code-atoms'
 import ImpressumPopup from '../Popups/Impressum'
 import LoadUrlPopup from '../Popups/LoadUrl'
@@ -29,7 +29,7 @@ import ToolsPopup from '../Popups/Tools'
 import { mobileAtom } from '../settings/settings-atoms'
 import { SettingsPopup } from '../settings/SettingsPopup'
 import { setImportUrlAndProjectAtom } from '../store/import-atoms'
-import { projectAtom, projectsAtom } from '../store/project-atoms'
+import { currentProjectAtom, projectsAtom, visibleProjectsAtom } from '../store/project-atoms'
 import { save } from '../utils/SaveToFile'
 import { Dropdown } from './Dropdown'
 import { NavButton } from './NavButton'
@@ -155,8 +155,8 @@ export function Menu({
   codeMirror: boolean
   setCodeMirror: Dispatch<SetStateAction<boolean>>
 }) {
-  const [{ data: projects }] = useAtom(projectsAtom)
-  const [project, setProject] = useAtom(projectAtom)
+  const [visibleProjects] = useAtom(visibleProjectsAtom)
+  const [project, setProject] = useAtom(currentProjectAtom)
   const [code] = useAtom(codeAtom)
 
   // state for handling the dropdown menus
@@ -178,20 +178,23 @@ export function Menu({
 
   return (
     <div className="menu">
-      <select
-        name="leanVersion"
-        value={project}
-        onChange={(ev) => {
-          setProject(ev.target.value)
-          console.log(`set Lean project to: ${ev.target.value}`)
-        }}
-      >
-        {projects.map((proj) => (
-          <option key={proj.folder} value={proj.folder}>
-            {proj.config.name}
-          </option>
-        ))}
-      </select>
+      {project && (
+        <select
+          name="leanVersion"
+          value={project.folder}
+          onChange={(ev) => {
+            setProject(ev.target.value)
+            console.log(`set Lean project to: ${ev.target.value}`)
+          }}
+        >
+          {project.folder}
+          {visibleProjects.map((proj) => (
+            <option key={proj.folder} value={proj.folder}>
+              {proj.config.name}
+            </option>
+          ))}
+        </select>
+      )}
       {mobile && (
         <NavButton
           icon={faCode}
@@ -288,7 +291,13 @@ export function Menu({
       {hasImpressum && (
         <ImpressumPopup open={impressumOpen} handleClose={() => setImpressumOpen(false)} />
       )}
-      <ToolsPopup open={toolsOpen} handleClose={() => setToolsOpen(false)} project={project} />
+      {project && (
+        <ToolsPopup
+          open={toolsOpen}
+          handleClose={() => setToolsOpen(false)}
+          project={project.folder}
+        />
+      )}
       <SettingsPopup
         open={settingsOpen}
         handleClose={() => setSettingsOpen(false)}

client/src/navigation/Navigation.tsx

@@ -1,29 +1,10 @@
 import { atom } from 'jotai'
 import { atomWithQuery } from 'jotai-tanstack-query'
 
+import { LeanWebProject } from '../api/project-types'
 import { urlArgsAtom, urlArgsStableAtom } from './url-atoms'
 
-/* An example a project provides */
-export interface Example {
-  file: string
-  name: string
-}
-
-/* A project's user configuration */
-export type ProjectConfig = {
-  name: string
-  hidden: boolean
-  default: boolean
-  examples: Example[]
-}
-
-/* A project */
-export type Project = {
-  folder: string
-  config: ProjectConfig
-}
-
-const projectsQueryAtom = atomWithQuery<Project[]>((get) => ({
+const projectsQueryAtom = atomWithQuery<LeanWebProject[]>((get) => ({
   queryKey: ['projects'],
   queryFn: async () => {
     const res = await fetch(`/api/projects`)
@@ -32,7 +13,7 @@ const projectsQueryAtom = atomWithQuery<Project[]>((get) => ({
 }))
 
 /** Sort alphabetically while the `default` project always comes first */
-function sortProjects(p: Project, q: Project): number {
+function sortProjects(p: LeanWebProject, q: LeanWebProject): number {
   if (p.config.default) return -1
   if (q.config.default) return 1
   return p.config.name.localeCompare(q.config.name)
@@ -44,32 +25,50 @@ export const projectsAtom = atom((get) => {
   return { ...query, data: query.data?.sort(sortProjects) ?? [] }
 })
 
-export const defaultProjectFolderAtom = atom((get) => {
+export const defaultProjectAtom = atom((get) => {
   const projects = get(projectsAtom).data
-  if (projects.length === 0) return 'MathlibDemo' // TODO: is this correct?
+  if (projects.length === 0) return null
   const defaultProjects = projects.filter((it) => it.config.default)
 
   if (defaultProjects.length === 0) {
     console.warn(`Expected exactly one default project, but found none.`)
-    return projects[0].folder
+    return projects[0]
   }
   if (defaultProjects.length > 1) {
     console.error(`Expected exactly one default project, but found ${defaultProjects.length}`)
   }
-  return defaultProjects[0].folder
+  return defaultProjects[0]
 })
 
 /** The currently selected project */
-export const projectAtom = atom(
+export const currentProjectAtom = atom(
   (get) => {
-    const urlArgs = get(urlArgsStableAtom)
-    return urlArgs.project ?? get(defaultProjectFolderAtom)
+    const urlArgProject = get(urlArgsStableAtom).project
+    const defaultProject = get(defaultProjectAtom)
+    const allProjects = get(projectsAtom).data
+    if (!urlArgProject) return defaultProject
+    if (!urlArgProject) return defaultProject
+    return (
+      allProjects.find((it) => it.folder.toLowerCase() == urlArgProject.toLowerCase()) ??
+      defaultProject
+    )
   },
   (get, set, project: string) => {
     const urlArgs = get(urlArgsStableAtom)
+    const defaultProject = get(defaultProjectAtom)
     set(urlArgsAtom, {
       ...urlArgs,
-      project: project !== get(defaultProjectFolderAtom) ? project : undefined,
+      project:
+        defaultProject == undefined || project !== defaultProject.folder ? project : undefined,
     })
   },
 )
+
+/** Visible projects */
+export const visibleProjectsAtom = atom((get) => {
+  const current = get(currentProjectAtom)
+  const visible = get(projectsAtom).data.filter(
+    (it) => !it.config.hidden || (current && it.folder == current.folder),
+  )
+  return visible
+})

client/src/store/project-atoms.ts

@@ -24,6 +24,6 @@
     /* Performance */
     "skipLibCheck": true
   },
-  "include": ["src"],
+  "include": ["src", "config.ts"],
   "exclude": ["node_modules"]
 }