From 8e27e217fa4b6fbf34f588e70036fa7a21df5183 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 20 Dec 2011 19:02:04 -0500 Subject: Redo HTML context classification, to keep regular tags out of and --- demo/batchFun.ur | 2 +- demo/more/dlist.ur | 14 +++++++------- demo/more/dlist.urs | 6 +++--- demo/more/grid.ur | 2 +- 4 files changed, 12 insertions(+), 12 deletions(-) (limited to 'demo') diff --git a/demo/batchFun.ur b/demo/batchFun.ur index 2b54a426..d69d68af 100644 --- a/demo/batchFun.ur +++ b/demo/batchFun.ur @@ -85,7 +85,7 @@ functor Make(M : sig

- {@mapX [colMeta] [[Body, Tr]] + {@mapX [colMeta] [tr] (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m => ) M.fl M.cols} diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur index 884ab8a1..a5af8d25 100644 --- a/demo/more/dlist.ur +++ b/demo/more/dlist.ur @@ -66,7 +66,7 @@ fun replace [t] dl ls = set dl (Nonempty {Head = Cons (x, hd), Tail = tlS}) end -fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos len dl = +fun renderDyn [ctx] [ctx ~ [Dyn]] [t] (f : t -> position -> xml (ctx ++ [Dyn]) [] []) filter pos len dl = return @@ -119,8 +119,8 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] end}/> -fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) - : option int -> list (t * position) -> xml (ctx ++ body) [] [] = +fun renderFlat [ctx] [ctx ~ [Dyn]] [t] (f : t -> position -> xml (ctx ++ [Dyn]) [] []) + : option int -> list (t * position) -> xml (ctx ++ [Dyn]) [] [] = let fun renderFlat' len ls = case len of @@ -186,10 +186,10 @@ fun sort [t] (cmp : t -> t -> signal bool) = sort' end -fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool, - Sort : signal (option (t -> t -> signal bool)), - StartPosition : signal (option int), - MaxLength : signal (option int)}) dl = +fun render [ctx] [ctx ~ [Dyn]] [t] f (r : {Filter : t -> signal bool, + Sort : signal (option (t -> t -> signal bool)), + StartPosition : signal (option int), + MaxLength : signal (option int)}) dl = dlist t -> signal int val numPassing : t ::: Type -> (t -> signal bool) -> dlist t -> signal int val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dlist t -> signal acc -val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type - -> (t -> position -> xml (ctx ++ body) [] []) +val render : ctx ::: {Unit} -> [ctx ~ [Dyn]] => t ::: Type + -> (t -> position -> xml (ctx ++ [Dyn]) [] []) -> {StartPosition : signal (option int), MaxLength : signal (option int), Filter : t -> signal bool, Sort : signal (option (t -> t -> signal bool)) (* <= *)} -> dlist t - -> xml (ctx ++ body) [] [] + -> xml (ctx ++ [Dyn]) [] [] diff --git a/demo/more/grid.ur b/demo/more/grid.ur index 9375e811..dd0cb813 100644 --- a/demo/more/grid.ur +++ b/demo/more/grid.ur @@ -125,7 +125,7 @@ functor Make(M : sig

Id	{[m.Nam]}

- {@mapX2 [fst3] [colMeta M.row] [[Body, Tr]] + {@mapX2 [fst3] [colMeta M.row] [tr] (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] data (meta : colMeta M.row p) =>

			-- cgit v1.2.3