annotate navbar.ur @ 20:554e342665fe

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