annotate navigation.urs @ 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 48a4180171b0
children
rev   line source
kkallio@7 1 (* A navigation is a collection of navigation bars (menus) made of links of
kkallio@7 2 * which up to one may be marked as active, optional isolated links not part of
kkallio@7 3 * menu bars and also optional message or status zones containing xml. The
kkallio@7 4 * programmer can provide a way to format these elements into a collection of
kkallio@7 5 * pieces of xml which can then be inserted into themes. *)
kkallio@7 6
kkallio@7 7 functor Make(M : sig
kkallio@7 8 con linkPos :: {Unit}
kkallio@7 9 (* The collection of isolated links. Should be inferred. *)
kkallio@7 10
kkallio@7 11 val linkFolder : folder linkPos
kkallio@7 12 (* Implementation detail; should be inferred. *)
kkallio@7 13
kkallio@7 14 con navbarPos :: {Unit}
kkallio@7 15 (* The collection of navbars. *)
kkallio@7 16
kkallio@7 17 con msgPos :: {Unit}
kkallio@7 18 (* The collection of optional status or message xml pieces. *)
kkallio@7 19
kkallio@7 20 val msgFolder : folder msgPos
kkallio@7 21 (* Implementation detail; should be inferred. *)
kkallio@7 22
kkallio@7 23 con linkStyles :: {Type} = mapU (option css_class) linkPos
kkallio@7 24 (* The collection of isolated links, with an optional CSS class
kkallio@7 25 * which will be applied to that link. *)
kkallio@7 26
kkallio@7 27 con themePos :: {Unit}
kkallio@7 28 (* The positions in the theme to generate xml for. *)
kkallio@7 29
kkallio@7 30 val linkStyles : $linkStyles
kkallio@7 31 (* The input optional link positions and styles. *)
kkallio@7 32
kkallio@7 33 val formatNav : $(mapU xbody navbarPos) -> $(mapU xbody linkPos) -> $(mapU xbody msgPos)
kkallio@7 34 -> $(mapU xbody themePos)
kkallio@7 35 (* The way to format the collections of navbars, links and message
kkallio@7 36 * zones into pieces of xml for the theme positions. *)
kkallio@7 37
kkallio@7 38 end) : sig
kkallio@7 39
kkallio@7 40 con modeLs :: {Type} -> Type = fn r :: {Type} => $(map Navbar.mode r)
kkallio@7 41 con barLs :: {Type} -> Type = fn r :: {Type} => $(map Navbar.navBar r)
kkallio@7 42
kkallio@7 43 con linkLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option Navbar.navItem) r)
kkallio@7 44 con msgLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option xbody) r)
kkallio@7 45
kkallio@7 46 class shape
kkallio@7 47
kkallio@7 48 val shape_npos : shape $(mapU xbody M.navbarPos)
kkallio@7 49
kkallio@7 50 con crush :: {Type} -> Type = fn r :: {Type} => $(map (fn _ => xbody) r)
kkallio@7 51
kkallio@7 52 con navigation :: {Type} -> Type = fn m :: {Type} => {Nav : barLs m,
kkallio@7 53 Link : linkLs M.linkPos,
kkallio@7 54 Msg : msgLs M.msgPos}
kkallio@7 55 (* Represents a complete navigation ensemble. *)
kkallio@7 56
kkallio@7 57 val mkNav : m ::: {Type} -> shape (crush m) -> modeLs m -> barLs m
kkallio@7 58 -> linkLs M.linkPos -> msgLs M.msgPos
kkallio@7 59 -> navigation m
kkallio@7 60 (* Builds a navigation from input elements of navbars, isolated links and messages. *)
kkallio@7 61
kkallio@7 62 val toXml : m ::: {Type} -> folder m -> shape (crush m) -> modeLs m
kkallio@7 63 -> navigation m -> $(mapU xbody M.themePos)
kkallio@7 64 (* Renders a navigation to xml pieces suitable for inclusion in a theme. *)
kkallio@7 65
kkallio@7 66 end