Pass the name of an example to bypass the selector screen

justfile

@@ -104,8 +104,8 @@ clean_resvg:
 clean_all: clean clean_raylib clean_bundler clean_resvg clean_static_lib
 
 # run the demo executable
-run: build
-    .lake/build/bin/raylean
+run *demoName: build
+    .lake/build/bin/raylean {{demoName}}
 
 build-bundler:
     mkdir -p {{parent_directory(makebundle_output_path)}}

lean/Examples/Selector.lean

@@ -19,6 +19,16 @@ inductive Demo where
 
 def Demo.all := allElements Demo
 
+def stringToDemo (s : String) : Option Demo :=
+  match s.trim.toLower with
+  | "jessica" => some .jessica
+  | "window" => some .window
+  | "platformer2d" => some .platformer2d
+  | "cube3d" => some .cube3d
+  | "inputkeys" => some .inputKeys
+  | "basicecs" => some .basicECS
+  | _ => none
+
 def screenWidth : Nat := 800
 def optionHeight : Nat := 80
 def screenHeight : Nat := Demo.all.size * optionHeight
@@ -88,4 +98,10 @@ def selector : IO Unit := do
   setTargetFPS 60
   start
 
+/-- Directly launch a demo by name, otherwise start the selector --/
+def tryLaunchDemo (name : String) : IO Unit :=
+  match stringToDemo name with
+  | none => selector
+  | some d => mkDemoInfo d |>.start
+
 end Selector

lean/Main.lean

@@ -1,3 +1,6 @@
 import «Examples».Selector
 
-def main : IO Unit := Selector.selector
+def main (args : List String) : IO Unit := do
+  match args with
+  | (demoName :: _) => Selector.tryLaunchDemo demoName
+  | _ => Selector.selector