[ doc ] adjusted select tutorial

stefan-hoeck · Jul 18, 2023 · ccbfd49 · ccbfd49
1 parent 423e4ab
commit ccbfd49
Show file tree

Hide file tree

Showing 9 changed files with 266 additions and 174 deletions.
diff --git a/docs/docs.ipkg b/docs/docs.ipkg
@@ -3,8 +3,9 @@ version    = 0.0.1
 authors    = "Stefan Höck"
 depends    = dom-mvc
            , contrib
-           , rio
+           , finite
            , monocle
+           , rio
 
 opts       = "--codegen javascript"
 

diff --git a/docs/src/Examples/Balls.md b/docs/src/Examples/Balls.md
@@ -150,8 +150,8 @@ milliseconds.
 ```idris
 public export
 data BallsEv : Type where
-  Init  : BallsEv
-  Run   : BallsEv
+  BallsInit  : BallsEv
+  Run        : BallsEv
   NumIn : Either String Nat -> BallsEv
   Next  : DTime -> BallsEv
 
@@ -279,7 +279,7 @@ showFPS n =
    in "FPS: \{show val}"
 
 adjST : BallsEv -> BallsST -> BallsST
-adjST Init      _ = init
+adjST BallsInit _ = init
 adjST Run       s = {balls := maybe s.balls initialBalls s.numBalls} s
 adjST (NumIn x) s = {numBalls := eitherToMaybe x} s
 adjST (Next m)  s = case s.count of
@@ -294,7 +294,7 @@ displayST s =
   ]
 
 displayEv : BallsEv -> DOMUpdate BallsEv
-displayEv Init      = child exampleDiv content
+displayEv BallsInit = child exampleDiv content
 displayEv Run       = NoAction
 displayEv (NumIn x) = validate txtCount x
 displayEv (Next m)  = NoAction
@@ -304,8 +304,8 @@ display e s = displayEv e :: displayST s
 
 export
 runBalls : Has BallsEv es => SHandler es -> BallsEv -> BallsST -> JSIO BallsST
-runBalls h Init s = do
-  s2   <- injectDOM adjST display h Init s
+runBalls h BallsInit s = do
+  s2   <- injectDOM adjST display h BallsInit s
   stop <- animate (h . inject . Next)
   pure $ {cleanUp := stop} s2
 runBalls h e s = injectDOM adjST display h e s

diff --git a/docs/src/Examples/CSS.md b/docs/src/Examples/CSS.md
@@ -43,8 +43,8 @@ be found in the corresponding submodules).
 
 ```idris
 export
-allRules : List (Rule 1)
-allRules =
+rules : List (Rule 1)
+rules =
      coreCSS
   ++ Balls.css
   ++ Fractals.css

diff --git a/docs/src/Examples/Fractals.idr b/docs/src/Examples/Fractals.idr
@@ -54,11 +54,11 @@ readDelay =
 
 public export
 data FractEv : Type where
-  Init   : FractEv
-  Iter   : Either String Iterations -> FractEv
-  Redraw : Either String RedrawDelay -> FractEv
-  Run    : FractEv
-  Inc    : DTime -> FractEv
+  FractInit : FractEv
+  Iter      : Either String Iterations -> FractEv
+  Redraw    : Either String RedrawDelay -> FractEv
+  Run       : FractEv
+  Inc       : DTime -> FractEv
 
 public export
 record FractST where
@@ -108,7 +108,7 @@ rotate []     = []
 rotate (h::t) = t ++ [h]
 
 adjST : FractEv -> FractST -> FractST
-adjST Init       s = init
+adjST FractInit  s = init
 adjST (Iter x)   s = {itersIn  := eitherToMaybe x} s
 adjST (Redraw x) s = {redrawIn := eitherToMaybe x} s
 adjST (Inc dt)   s =
@@ -137,7 +137,7 @@ displayST s =
   ]
 
 displayEv : FractEv -> DOMUpdate FractEv
-displayEv Init       = child exampleDiv content
+displayEv FractInit  = child exampleDiv content
 displayEv (Iter x)   = validate txtIter x
 displayEv (Redraw x) = validate txtRedraw x
 displayEv Run        = NoAction
@@ -148,8 +148,8 @@ display e s = displayEv e :: displayST s
 
 export
 runFract : Has FractEv es => SHandler es -> FractEv -> FractST -> JSIO FractST
-runFract h Init s = do
-  s2   <- injectDOM adjST display h Init s
+runFract h FractInit s = do
+  s2   <- injectDOM adjST display h FractInit s
   stop <- animate (h . inject . Inc)
   pure $ {cleanUp := stop} s2
 runFract h e s = injectDOM adjST display h e s
diff --git a/docs/src/Examples/MathGame.md b/docs/src/Examples/MathGame.md
@@ -44,10 +44,10 @@ data Language = EN | DE
 
 public export
 data MathEv : Type where
-  Lang  : Language -> MathEv
-  Check : MathEv
-  Init  : MathEv
-  Inp   : String -> MathEv
+  Lang     : Language -> MathEv
+  Check    : MathEv
+  MathInit : MathEv
+  Inp      : String -> MathEv
 
 lang : String -> MathEv
 lang "de" = Lang DE
@@ -214,7 +214,7 @@ content l =
              ] [Text $ checkAnswerStr l]
 
     , button [ Id newBtn
-             , onClick Init
+             , onClick MathInit
              , classes [widget,btn]
              ] [Text $ newGameStr l]
 
@@ -324,7 +324,7 @@ the input text field:
 adjST : MathEv -> MathST -> MathST
 adjST (Lang x) = {lang := x}
 adjST Check    = checkAnswer
-adjST Init     = id
+adjST MathInit = id
 adjST (Inp s)  = {answer := s}
 
 displayST : MathST -> List (DOMUpdate MathEv)
@@ -341,15 +341,15 @@ displayST s =
 displayEv : MathEv -> DOMUpdate MathEv
 displayEv (Lang x) = child exampleDiv (content x)
 displayEv Check    = Value resultIn ""
-displayEv Init     = child exampleDiv (content init.lang)
+displayEv MathInit = child exampleDiv (content init.lang)
 displayEv (Inp _)  = NoAction
 
 display : MathEv -> MathST -> List (DOMUpdate MathEv)
 display e s = displayEv e :: displayST s
 
 export
 runMath : Has MathEv es => SHandler es -> MathEv -> MathST -> JSIO MathST
-runMath h Init s = randomGame s.lang >>= injectDOM adjST display h Init
+runMath h MathInit s = randomGame s.lang >>= injectDOM adjST display h MathInit
 runMath h e    s = injectDOM adjST display h e s
 ```
 

diff --git a/docs/src/Examples/Performance.md b/docs/src/Examples/Performance.md
@@ -64,7 +64,7 @@ PosNat = Subset Nat IsSucc
 
 public export
 data PerfEv : Type where
-  Init       : PerfEv
+  PerfInit   : PerfEv
   NumChanged : Either String PosNat -> PerfEv
   Reload     : PerfEv
   Set        : Nat -> PerfEv
@@ -188,7 +188,7 @@ convenient to use.
 
 ```idris
 adjST : PerfEv -> PerfST -> PerfST
-adjST Init           = const init
+adjST PerfInit       = const init
 adjST (NumChanged e) = {num := eitherToMaybe e}
 adjST Reload         = {sum := 0}
 adjST (Set k)        = {sum $= (+k)}
@@ -197,7 +197,7 @@ displayST : PerfST -> List (DOMUpdate PerfEv)
 displayST s = [disabledM btnRun s.num, show out s.sum]
 
 displayEv : PerfEv -> PerfST -> DOMUpdate PerfEv
-displayEv Init           _ = child exampleDiv content
+displayEv PerfInit       _ = child exampleDiv content
 displayEv (NumChanged e) _ = validate natIn e
 displayEv (Set k)        _ = disabled (btnRef k) True
 displayEv Reload         s = maybe NoAction (child buttons . btns) s.num

diff --git a/docs/src/Examples/Reset.md b/docs/src/Examples/Reset.md
@@ -38,8 +38,8 @@ our event type will be a function on integers:
 ```idris
 public export
 data ResetEv : Type where
-  Init : ResetEv
-  Mod  : (Int8 -> Int8) -> ResetEv
+  ResetInit : ResetEv
+  Mod       : (Int8 -> Int8) -> ResetEv
 ```
 
 ## View
@@ -101,7 +101,7 @@ that produces no output of interest):
 
 ```idris
 adjST : ResetEv -> Int8 -> Int8
-adjST Init    n = 0
+adjST ResetInit n = 0
 adjST (Mod f) n = f n
 
 displayST : Int8 -> List (DOMUpdate ResetEv)
@@ -113,8 +113,8 @@ displayST n =
   ]
 
 display : ResetEv -> Int8 -> List (DOMUpdate ResetEv)
-display Init    n = child exampleDiv content :: displayST n
-display (Mod f) n = displayST n
+display ResetInit n = child exampleDiv content :: displayST n
+display (Mod f)   n = displayST n
 
 export
 runReset : Has ResetEv es => SHandler es -> ResetEv -> Int8 -> JSIO Int8