(* A navigation is a collection of navigation bars (menus) made of links of
 * which up to one may be marked as active, optional isolated links not part of
 * menu bars and also optional message or status zones containing xml.  The
 * programmer can provide a way to format these elements into a collection of
 * pieces of xml which can then be inserted into themes. *)

functor Make(M : sig
                 con linkPos :: {Unit}
                 (* The collection of isolated links.  Should be inferred. *)

                 val linkFolder : folder linkPos
                 (* Implementation detail; should be inferred. *) 

                 con navbarPos :: {Unit}
                 (* The collection of navbars. *)
 
                 con msgPos :: {Unit}
                 (* The collection of optional status or message xml pieces. *)

                 val msgFolder : folder msgPos
                 (* Implementation detail; should be inferred. *)

                 con linkStyles :: {Type} = mapU (option css_class) linkPos
                 (* The collection of isolated links, with an optional CSS class
                  * which will be applied to that link. *) 

                 con themePos :: {Unit}
                 (* The positions in the theme to generate xml for. *)

                 val linkStyles : $linkStyles
                 (* The input optional link positions and styles. *)

                 val formatNav : $(mapU xbody navbarPos) -> $(mapU xbody linkPos) -> $(mapU xbody msgPos)
                                 -> $(mapU xbody themePos)
                 (* The way to format the collections of navbars, links and message
                  * zones into pieces of xml for the theme positions. *)

             end) : sig

    con modeLs :: {Type} -> Type = fn r :: {Type} => $(map Navbar.mode r)
    con barLs :: {Type} -> Type = fn r :: {Type} => $(map Navbar.navBar r)

    con linkLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option Navbar.navItem) r)
    con msgLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option xbody) r)

    class shape

    val shape_npos : shape $(mapU xbody M.navbarPos)

    con crush :: {Type} -> Type = fn r :: {Type} => $(map (fn _ => xbody) r) 

    con navigation :: {Type} -> Type = fn m :: {Type} => {Nav : barLs m,
                                                          Link : linkLs M.linkPos,
                                                          Msg : msgLs M.msgPos}
    (* Represents a complete navigation ensemble. *)                                                     

    val mkNav : m ::: {Type} -> shape (crush m) -> modeLs m -> barLs m
                -> linkLs M.linkPos -> msgLs M.msgPos
                -> navigation m
    (* Builds a navigation from input elements of navbars, isolated links and messages. *) 

    val toXml : m ::: {Type} -> folder m -> shape (crush m) -> modeLs m 
                -> navigation m -> $(mapU xbody M.themePos)
    (* Renders a navigation to xml pieces suitable for inclusion in a theme. *)

end