stuff

DOCUMENTATION.md

@@ -213,7 +213,7 @@ Notation for naturals is `\\N`."
 
 The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
 
-## Using Dev Containers
+## VSCode Dev Containers
 
 1.  **Install Docker and Dev Containers** *(once)*:<br/>
     See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
@@ -225,13 +225,14 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
     * Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
     * a message appears prompting you to install the "Dev Containers" extension (by Microsoft).
 
-2.  **Open Project in Dev Container** **(everytime)**:<br/>
+2.  **Open Project in Dev Container** *(everytime)*:<br/>
     Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
     A message appears asking you to "Reopen in Container".
 
-    * The first start will take a while, ca. 1-5 minutes. After the first
+    * The first start will take a while, ca. 2-10 minutes. After the first
       start this should be very quickly.
-    * Afterwards, go to your browser and open http://localhost:3000/#/g/local/game.
+    * Once built, it should open a tab "Simple Browser" inside VSCode displaying
+      the game. (Alternatively, open http://localhost:3000 in your browser).
 
 3.  **Editing Files** *(everytime)*:<br/>
     After editing some files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`.

client/src/components/infoview/main.tsx

@@ -335,7 +335,11 @@ export function CommandLineInterface(props: { world: string, level: number, data
 
   // Scroll to the end of the proof if it is updated.
   React.useEffect(() => {
-    proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
+    if (proof?.length > 1) {
+      proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
+    } else {
+      proofPanelRef.current?.scrollTo(0,0)
+    }
   }, [proof])
 
   // Scroll to element if selection changes

client/src/components/world_tree.css

@@ -51,15 +51,13 @@ svg .disabled {
 .world-selection-menu {
   padding: .5em 1em;
   position: absolute;
-  right: 0;
+  right: 1em;
   top: 1em;
   /* margin: 1em; */
   /* border: 1px solid var(--clr-primary); */
-  border-bottom: 1px solid var(--clr-primary);
-  border-left: 1px solid var(--clr-primary);
-  border-top: 1px solid var(--clr-primary);
+  border: 1px solid var(--clr-primary);
   background-color: #fff;
-  border-radius: .5em 0 0 .5em;
+  border-radius: .5em;
   filter: drop-shadow(4px 4px 5px rgba(0,0,0,0.5));
 }
 

client/src/components/world_tree.tsx

@@ -193,15 +193,15 @@ export function WorldSelectionMenu() {
   const dispatch = useAppDispatch()
 
   function label(x : number) {
-    return x == 0 ? 'none' : x == 1 ? 'lax' : 'regular'
+    return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
   }
 
   return <nav className="world-selection-menu">
     <div className="slider-wrap">
       <span className="difficulty-label">Game Rules</span>
       <Slider
         orientation="vertical"
-        title="Game Rules:&#10;- regular: 🔐 levels, 🔐 tactics&#10;- lax: 🔓 levels, 🔐 tactics&#10;- none: 🔓 levels, 🔓 tactics"
+        title="Game Rules:&#10;- regular: 🔐 levels, 🔐 tactics&#10;- relaxed: 🔓 levels, 🔐 tactics&#10;- none: 🔓 levels, 🔓 tactics"
         min={0} max={2}
         aria-label="Game Rules"
         defaultValue={difficulty}

package.json

@@ -67,8 +67,11 @@
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
+    "start_single": "concurrently -n server,client -c blue,green \"npm run start_server_single\" \"npm run start_client_single\"",
     "start_server": "cd server && lake build && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
     "start_client": "cross-env NODE_ENV=development webpack-dev-server --hot",
+    "start_server_single": "cd server && lake build && cross-env NODE_ENV=development LEAN4GAME_SINGLE_GAME=true nodemon -e mjs --exec \"node ./index.mjs\"",
+    "start_client_single": "cross-env NODE_ENV=development LEAN4GAME_SINGLE_GAME=true webpack-dev-server --hot",
     "build": "cross-env NODE_ENV=production webpack",
     "production": "cross-env NODE_ENV=production node server/index.mjs",
     "build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag g/hhu-adam/robo && rm -rf ./Robo",

webpack.config.js

@@ -5,7 +5,7 @@ const WebpackShellPluginNext = require('webpack-shell-plugin-next');
 
 module.exports = env => {
 
-  const single_game = process.env.LOCAL_GAME
+  const single_game = process.env.LEAN4GAME_SINGLE_GAME
 
 
   const environment = process.env.NODE_ENV