From 6f92d6138148e9222052f681b589c8d015750c47 Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Thu, 9 Nov 2023 15:26:53 +0100
Subject: [PATCH] fix redirect from landing page in dev container #145

---
 client/src/index.tsx       | 56 ++++++++++++++++++++++++--------------
 client/src/index_local.tsx | 55 -------------------------------------
 env.d.ts                   | 10 +++++++
 3 files changed, 46 insertions(+), 75 deletions(-)
 delete mode 100644 client/src/index_local.tsx
 create mode 100644 env.d.ts

diff --git a/client/src/index.tsx b/client/src/index.tsx
index 2b593c6..85c6c83 100644
--- a/client/src/index.tsx
+++ b/client/src/index.tsx
@@ -1,29 +1,45 @@
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
+import * as React from 'react'
+import { createRoot } from 'react-dom/client'
+import App from './app'
 import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
-  createHashRouter,
-  RouterProvider,
-  Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
+import { store } from './state/store'
+import { Provider } from 'react-redux'
+import type { RouteObject } from "react-router"
+import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
+import ErrorPage from './components/error_page'
+import Welcome from './components/welcome'
+import LandingPage from './components/landing_page'
+import Level from './components/level'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+
 
 monacoSetup()
 
+// // Do not show the landing page in the dev-container context
+// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? {
+//   path: "/",
+//   loader: () => redirect("/g/local/game")
+// } : {
+//   path: "/",
+//   element: <LandingPage />,
+// }
+
+
+// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
+// `/g/local/game`. This is used for the devcontainer setup
+let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
+let root_object: RouteObject = single_game ? {
+  path: "/",
+  loader: () => redirect("/g/local/game")
+} : {
+  path: "/",
+  element: <LandingPage />,
+}
+
 const router = createHashRouter([
+  root_object,
   {
-    path: "/",
-    element: <LandingPage />,
-  },
-  {
+    // For backwards compatibility
     path: "/game/nng",
     loader: () => redirect("/g/hhu-adam/NNG4")
   },
diff --git a/client/src/index_local.tsx b/client/src/index_local.tsx
deleted file mode 100644
index 9328768..0000000
--- a/client/src/index_local.tsx
+++ /dev/null
@@ -1,55 +0,0 @@
-// This file is a copy of `index.tsx` where the path "/" is redirected to "/g/local/game".
-// It is used for the dev. setup where there is only one game in a folder called `game`.
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
-import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
-  createHashRouter,
-  RouterProvider,
-  Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
-
-monacoSetup()
-
-const router = createHashRouter([
-  {
-    path: "/",
-    loader: () => redirect("/g/local/game")
-  },
-  {
-    path: "/g/:owner/:repo",
-    element: <App />,
-    errorElement: <ErrorPage />,
-    children: [
-      {
-        path: "/g/:owner/:repo",
-        element: <Welcome />,
-      },
-      {
-        path: "/g/:owner/:repo/world/:worldId/level/:levelId",
-        element: <Level />,
-      },
-    ],
-  },
-]);
-
-const container = document.getElementById('root');
-const root = createRoot(container!);
-root.render(
-  <React.StrictMode>
-    <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
-    </Provider>
-  </React.StrictMode>
-);
diff --git a/env.d.ts b/env.d.ts
new file mode 100644
index 0000000..4d10cb9
--- /dev/null
+++ b/env.d.ts
@@ -0,0 +1,10 @@
+/// <reference types="vite/client" />
+
+interface ImportMetaEnv {
+  readonly VITE_LEAN4GAME_SINGLE: string
+  // more env variables...
+}
+
+interface ImportMeta {
+  readonly env: ImportMetaEnv
+}