summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 14:56:03 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 14:56:03 -0400
commit8ba030d9f3ca612405f36db1fc6b1fbaa08448b2 (patch)
treeff3523fe090bc22e677d6b9b4cce8673794b8cab
parent3bf0f6b7a465e3f24eff57633ee8aa3bbe41422a (diff)
Paging + filtering seemingly working, but runtime system isn't GCing signals properly, so performance goes south quickly
-rw-r--r--demo/more/dlist.ur23
1 files changed, 15 insertions, 8 deletions
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 277f1219..1e5b8020 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -83,15 +83,22 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) []
val pos = case prev of
None => headPos dl
| Some prev => tailPos prev tl tlTop
- val len = Option.mp (fn n => n - 1) len
in
- <xml><dyn signal={b <- filter v;
- return (if b then
- f v pos
- else
- <xml/>)}/>
- <dyn signal={tl' <- signal tl;
- return (render' (Some tl) tl' len)}/></xml>
+ <xml>
+ <dyn signal={b <- filter v;
+ return <xml>
+ {if b then
+ f v pos
+ else
+ <xml/>}
+ <dyn signal={tl' <- signal tl;
+ return (render' (Some tl) tl'
+ (if b then
+ Option.mp (fn n => n - 1) len
+ else
+ len))}/>
+ </xml>}/>
+ </xml>
end
fun skip pos hd =