diff demo/more/dlist.urs @ 951:103ac1792c41

Make filter argument to render, not create
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Sep 2009 14:27:00 -0400
parents da3ec6014d2f
children 07569af40069
line wrap: on
line diff
--- a/demo/more/dlist.urs	Thu Sep 17 13:44:08 2009 -0400
+++ b/demo/more/dlist.urs	Thu Sep 17 14:27:00 2009 -0400
@@ -1,7 +1,7 @@
 con dlist :: Type -> Type
 type position
 
-val create : t ::: Type -> {Filter : t -> signal bool} -> transaction (dlist t)
+val create : t ::: Type -> transaction (dlist t)
 val clear : t ::: Type -> dlist t -> transaction unit
 val append : t ::: Type -> dlist t -> t -> transaction position
 val delete : position -> transaction unit
@@ -10,5 +10,6 @@
 
 val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
              -> (t -> position -> xml (ctx ++ body) [] [])
+             -> {Filter : t -> signal bool}
              -> dlist t
              -> xml (ctx ++ body) [] []