Merge pull request #70 from stefan-hoeck/editor_iso

[ new ] view an editor through an isomorphism
stefan-hoeck · Apr 21, 2024 · fd0c4b3 · fd0c4b3
2 parents 4e1472a + 23f2dfb
commit fd0c4b3
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/extra/src/Web/MVC/Controller.idr b/extra/src/Web/MVC/Controller.idr
@@ -132,6 +132,11 @@ record Editor (i,st,ev,new : Type) where
   ||| Create an initial state from an optional value of type `new`
   toState : Maybe new -> st
 
+||| View an editor through an isomorphism.
+export
+newIso : Iso' n1 n2 -> Editor i st ev n1 -> Editor i st ev n2
+newIso i = {stToNew $= (map i.get_ .), toState $= (. map i.reverseGet)}
+
 ||| Utility for editors without initial command.
 export %inline
 noInit : i -> s -> Cmd e