Skip to content

Commit

Permalink
Pass the name of an example to bypass the selector screen
Browse files Browse the repository at this point in the history
For example:

```
just run jessica
```

will launch directly into 'Jessica Can't Swim'.

Passing a blank (whitespace or empty) argument will launch the example
selector as before.
  • Loading branch information
paulcadman committed Sep 6, 2024
1 parent b948e3f commit 65d761b
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 3 deletions.
4 changes: 2 additions & 2 deletions justfile
Original file line number Diff line number Diff line change
Expand Up @@ -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)}}
Expand Down
16 changes: 16 additions & 0 deletions lean/Examples/Selector.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
5 changes: 4 additions & 1 deletion lean/Main.lean
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 65d761b

Please sign in to comment.