|
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
|
