annotate navbar.ur @ 27:5905b56e0cd9

Adapt to new HTML contexts
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Dec 2011 21:04:21 -0500
parents d314d2ec3300
children d32fb0f7b137
rev   line source
kkallio@6 1 style active
kkallio@6 2 style last
kkallio@6 3
kkallio@6 4 datatype navItem = NavItem of string * url
kkallio@6 5
rmbruijn@24 6 fun name (NavItem (text, url)) = text
rmbruijn@24 7
kkallio@6 8 datatype navBar m = NavBar of (list navItem) * (list navItem)
kkallio@6 9 (* First list is items before the active item, second list is items at and after the active one.
kkallio@6 10 * If the second list is non-empty its head is the active item. Parameter mode is to avoid
kkallio@6 11 * double reverses coming from calling printingNavBar. *)
kkallio@6 12
kkallio@6 13 type build = unit
kkallio@6 14 type print = unit
kkallio@6 15
kkallio@6 16 class mode t = navBar t -> xbody
kkallio@6 17
kkallio@6 18 (* The case of special treatment for the last one seems common in themes. *)
kkallio@6 19 fun mapXLast [a ::: Type] [ctx ::: {Unit}] (f : a -> bool -> xml ctx [] []) (ls : list a) : (xml ctx [] []) =
kkallio@6 20 let
kkallio@6 21 fun mapXLast' ls =
kkallio@6 22 case ls of
kkallio@6 23 [] => <xml/>
kkallio@6 24 | x :: [] => <xml>{f x True}</xml>
kkallio@6 25 | x :: ls => <xml>{f x False}{mapXLast' ls}</xml>
kkallio@6 26 in
kkallio@6 27 mapXLast' ls
kkallio@6 28 end
kkallio@6 29
kkallio@6 30 fun navItemToXml css (NavItem (text, url)) =
kkallio@6 31 case css of
kkallio@6 32 None => <xml><a href={url} title={text}>{[text]}</a></xml>
kkallio@6 33 | Some cl => <xml><a class={cl} href={url} title={text}>{[text]}</a></xml>
kkallio@6 34
kkallio@6 35 fun navBarToXml' (NavBar (before, after)) =
kkallio@6 36 let
kkallio@6 37 fun navListToXml checkForLast =
kkallio@6 38 mapXLast (fn navItem lst =>
kkallio@6 39 let
kkallio@6 40 val linkXml = navItemToXml None navItem
kkallio@6 41 in
kkallio@6 42 if checkForLast && lst then
kkallio@6 43 <xml><li class={last}>{linkXml}</li></xml>
kkallio@6 44 else
kkallio@6 45 <xml><li>{linkXml}</li></xml>
kkallio@6 46 end)
kkallio@6 47 in
kkallio@6 48 case after of
kkallio@6 49 [] => <xml>{navListToXml True before}</xml>
kkallio@6 50 | act :: tl =>
kkallio@6 51 <xml>
kkallio@6 52 {navListToXml False before}
kkallio@6 53 {case tl of
kkallio@6 54 [] => <xml><li class={last}>{navItemToXml (Some active) act}</li></xml>
kkallio@6 55 | _ =>
kkallio@6 56 <xml>
kkallio@6 57 <li>{navItemToXml (Some active) act}</li>
kkallio@6 58 {navListToXml True tl}
kkallio@6 59 </xml>}
kkallio@6 60 </xml>
kkallio@6 61 end
kkallio@6 62
kkallio@6 63 fun printingNavBar (NavBar (before, after)) =
kkallio@6 64 NavBar (List.rev before, List.rev after)
kkallio@6 65
kkallio@6 66 fun navBarToXml [t ::: Type] (m : mode t) = m
kkallio@6 67
kkallio@6 68 fun navToXml_build (n : navBar build) : xbody =
kkallio@6 69 navBarToXml' (printingNavBar n)
kkallio@6 70
kkallio@6 71 fun navToXml_print (n: navBar print) : xbody =
kkallio@6 72 navBarToXml' n
kkallio@6 73
kkallio@6 74 val emptyNavBar = NavBar ([], [])
kkallio@6 75
kkallio@6 76 fun mkNavItem text url =
kkallio@6 77 NavItem (text, url)
kkallio@6 78
kkallio@6 79 fun navAdd navItem navBar =
kkallio@6 80 case navBar of
kkallio@6 81 NavBar (before, []) => NavBar (navItem :: before, [])
kkallio@6 82 | NavBar (before, after) => NavBar (before, navItem :: after)
kkallio@6 83
kkallio@6 84 fun navAddActive navItem navBar =
kkallio@6 85 case navBar of
kkallio@6 86 NavBar (before, []) => NavBar (before, navItem :: [])
kkallio@6 87 | NavBar (before, after) => NavBar (List.append after before, navItem :: [])