annotate navigation.ur @ 33:2e7f8f7d71d4

Update for Ur/Web's new tag name resolution
author Adam Chlipala <adam@chlipala.net>
date Thu, 21 Nov 2013 16:12:17 -0500
parents d32fb0f7b137
children
rev   line source
kkallio@7 1 functor Make(M : sig
kkallio@7 2 con linkPos :: {Unit}
kkallio@7 3 val linkFolder : folder linkPos
kkallio@7 4 con navbarPos :: {Unit}
kkallio@7 5 con msgPos :: {Unit}
kkallio@7 6 val msgFolder : folder msgPos
kkallio@7 7 con linkStyles :: {Type} = mapU (option css_class) linkPos
kkallio@7 8 con themePos :: {Unit}
kkallio@7 9 val linkStyles : $linkStyles
kkallio@7 10 val formatNav : $(mapU xbody navbarPos) -> $(mapU xbody linkPos) -> $(mapU xbody msgPos)
kkallio@7 11 -> $(mapU xbody themePos)
kkallio@7 12 end) = struct
kkallio@7 13
kkallio@7 14 open Navbar
kkallio@7 15
kkallio@7 16 con modeLs :: {Type} -> Type = fn r :: {Type} => $(map mode r)
kkallio@7 17 con barLs :: {Type} -> Type = fn r :: {Type} => $(map navBar r)
kkallio@7 18
kkallio@7 19 con linkLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option navItem) r)
kkallio@7 20 con msgLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option xbody) r)
kkallio@7 21
adam@32 22 con shape t = t -> $(mapU xbody M.navbarPos)
kkallio@7 23
kkallio@7 24 val shape_npos : shape $(mapU xbody M.navbarPos) = (fn x => x)
kkallio@7 25
kkallio@7 26 con crush :: {Type} -> Type = fn r :: {Type} => $(map (fn _ => xbody) r)
kkallio@7 27
kkallio@7 28 con navigation :: {Type} -> Type = fn m :: {Type} => {Nav : barLs m,
kkallio@7 29 Link : linkLs M.linkPos,
kkallio@7 30 Msg : msgLs M.msgPos}
kkallio@7 31
kkallio@7 32 fun mkNav [m ::: {Type}] (sh : shape (crush m)) (d : modeLs m) (n : barLs m)
kkallio@7 33 (l : linkLs M.linkPos) (msg : msgLs M.msgPos) =
kkallio@7 34 {Nav = n, Link = l, Msg = msg}
kkallio@7 35
kkallio@7 36 fun barsToXml [m ::: {Type}] (fl : folder m) (ms : modeLs m) (ns : barLs m) =
kkallio@7 37 @@Top.fold [fn r :: {Type} => $(map mode r) -> $(map navBar r) -> $(map (fn _ => xbody) r)]
kkallio@7 38 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest]
kkallio@7 39 (acc : _ -> _ -> _) rm rn =>
kkallio@7 40 {nm = @@navBarToXml [t] rm.nm rn.nm} ++ (acc (rm -- nm) (rn -- nm)))
kkallio@7 41 (fn _ _ => {}) [m] fl ms ns
kkallio@7 42
kkallio@7 43 fun linksToXml (l : linkLs M.linkPos) =
kkallio@7 44 let
kkallio@7 45 fun render s ol =
kkallio@7 46 case ol of
kkallio@7 47 None => <xml/>
kkallio@7 48 | Some l => navItemToXml s l
kkallio@7 49
kkallio@7 50 in
kkallio@7 51 @@Top.fold [fn u :: {Unit} => $(mapU (option navItem) u) -> $(mapU (option css_class) u) -> $(mapU xbody u)]
kkallio@7 52 (fn [nm :: Name] [t ::_] [rest :: {Unit}] [[nm] ~ rest]
kkallio@7 53 (acc : _ -> _ -> _) r s => {nm = render s.nm r.nm} ++ (acc (r -- nm) (s -- nm)))
kkallio@7 54 (fn _ _ => {}) [M.linkPos] M.linkFolder l M.linkStyles
kkallio@7 55 end
kkallio@7 56
kkallio@7 57 fun msgToXml (msg : msgLs M.msgPos) =
kkallio@7 58 let
kkallio@7 59 fun render om =
kkallio@7 60 case om of
kkallio@7 61 None => <xml/>
kkallio@7 62 | Some m => m
kkallio@7 63 in
kkallio@7 64 @@Top.mp [fn u => (option xbody)] [fn u => xbody]
kkallio@7 65 (fn [t :::_] => render) [M.msgPos] M.msgFolder msg
kkallio@7 66 end
kkallio@7 67
kkallio@7 68 fun toXml [m ::: {Type}] (fl : folder m) (sh : shape (crush m)) (d : modeLs m) {Nav = nav, Link = l, Msg = msg} =
kkallio@7 69 M.formatNav (sh (@@barsToXml [m] fl d nav)) (linksToXml l) (msgToXml msg)
kkallio@7 70
kkallio@7 71 end