kkallio@7: (* A navigation is a collection of navigation bars (menus) made of links of
kkallio@7:  * which up to one may be marked as active, optional isolated links not part of
kkallio@7:  * menu bars and also optional message or status zones containing xml.  The
kkallio@7:  * programmer can provide a way to format these elements into a collection of
kkallio@7:  * pieces of xml which can then be inserted into themes. *)
kkallio@7: 
kkallio@7: functor Make(M : sig
kkallio@7:                  con linkPos :: {Unit}
kkallio@7:                  (* The collection of isolated links.  Should be inferred. *)
kkallio@7: 
kkallio@7:                  val linkFolder : folder linkPos
kkallio@7:                  (* Implementation detail; should be inferred. *) 
kkallio@7: 
kkallio@7:                  con navbarPos :: {Unit}
kkallio@7:                  (* The collection of navbars. *)
kkallio@7:  
kkallio@7:                  con msgPos :: {Unit}
kkallio@7:                  (* The collection of optional status or message xml pieces. *)
kkallio@7: 
kkallio@7:                  val msgFolder : folder msgPos
kkallio@7:                  (* Implementation detail; should be inferred. *)
kkallio@7: 
kkallio@7:                  con linkStyles :: {Type} = mapU (option css_class) linkPos
kkallio@7:                  (* The collection of isolated links, with an optional CSS class
kkallio@7:                   * which will be applied to that link. *) 
kkallio@7: 
kkallio@7:                  con themePos :: {Unit}
kkallio@7:                  (* The positions in the theme to generate xml for. *)
kkallio@7: 
kkallio@7:                  val linkStyles : $linkStyles
kkallio@7:                  (* The input optional link positions and styles. *)
kkallio@7: 
kkallio@7:                  val formatNav : $(mapU xbody navbarPos) -> $(mapU xbody linkPos) -> $(mapU xbody msgPos)
kkallio@7:                                  -> $(mapU xbody themePos)
kkallio@7:                  (* The way to format the collections of navbars, links and message
kkallio@7:                   * zones into pieces of xml for the theme positions. *)
kkallio@7: 
kkallio@7:              end) : sig
kkallio@7: 
kkallio@7:     con modeLs :: {Type} -> Type = fn r :: {Type} => $(map Navbar.mode r)
kkallio@7:     con barLs :: {Type} -> Type = fn r :: {Type} => $(map Navbar.navBar r)
kkallio@7: 
kkallio@7:     con linkLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option Navbar.navItem) r)
kkallio@7:     con msgLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option xbody) r)
kkallio@7: 
kkallio@7:     class shape
kkallio@7: 
kkallio@7:     val shape_npos : shape $(mapU xbody M.navbarPos)
kkallio@7: 
kkallio@7:     con crush :: {Type} -> Type = fn r :: {Type} => $(map (fn _ => xbody) r) 
kkallio@7: 
kkallio@7:     con navigation :: {Type} -> Type = fn m :: {Type} => {Nav : barLs m,
kkallio@7:                                                           Link : linkLs M.linkPos,
kkallio@7:                                                           Msg : msgLs M.msgPos}
kkallio@7:     (* Represents a complete navigation ensemble. *)                                                     
kkallio@7: 
kkallio@7:     val mkNav : m ::: {Type} -> shape (crush m) -> modeLs m -> barLs m
kkallio@7:                 -> linkLs M.linkPos -> msgLs M.msgPos
kkallio@7:                 -> navigation m
kkallio@7:     (* Builds a navigation from input elements of navbars, isolated links and messages. *) 
kkallio@7: 
kkallio@7:     val toXml : m ::: {Type} -> folder m -> shape (crush m) -> modeLs m 
kkallio@7:                 -> navigation m -> $(mapU xbody M.themePos)
kkallio@7:     (* Renders a navigation to xml pieces suitable for inclusion in a theme. *)
kkallio@7: 
kkallio@7: end