view navbar.ur @ 21:30f9a763f5fb

Tweak TogglePanel signature
author Adam Chlipala <adam@chlipala.net>
date Sat, 24 Sep 2011 17:35:33 -0400
parents f17b869fbb71
children d314d2ec3300
line wrap: on
line source
style active
style last

datatype navItem = NavItem of string * url

datatype navBar m = NavBar of (list navItem) * (list navItem)
(* First list is items before the active item, second list is items at and after the active one.
 * If the second list is non-empty its head is the active item.  Parameter mode is to avoid
 * double reverses coming from calling printingNavBar. *)

type build = unit
type print = unit

class mode t = navBar t -> xbody

(* The case of special treatment for the last one seems common in themes. *)
fun mapXLast [a ::: Type] [ctx ::: {Unit}] (f : a -> bool -> xml ctx [] []) (ls : list a) : (xml ctx [] []) =
    let
        fun mapXLast' ls =
            case ls of
                [] => <xml/>
              | x :: [] => <xml>{f x True}</xml>
              | x :: ls => <xml>{f x False}{mapXLast' ls}</xml>
    in
        mapXLast' ls
    end

fun navItemToXml css (NavItem (text, url)) =
    case css of
        None => <xml><a href={url} title={text}>{[text]}</a></xml>
      | Some cl => <xml><a class={cl} href={url} title={text}>{[text]}</a></xml>

fun navBarToXml' (NavBar (before, after)) =
    let
        fun navListToXml checkForLast =
            mapXLast (fn navItem lst =>
                         let
                             val linkXml = navItemToXml None navItem
                         in
                             if checkForLast && lst then
                                 <xml><li class={last}>{linkXml}</li></xml>
                             else
                                 <xml><li>{linkXml}</li></xml>
                         end)
    in
        case after of
            [] => <xml>{navListToXml True before}</xml>
          | act :: tl =>
            <xml>
              {navListToXml False before}
              {case tl of
                   [] => <xml><li class={last}>{navItemToXml (Some active) act}</li></xml>
                 | _ =>
                   <xml>
                     <li>{navItemToXml (Some active) act}</li>
                     {navListToXml True tl}
                   </xml>}
            </xml>
    end

fun printingNavBar (NavBar (before, after)) =
    NavBar (List.rev before, List.rev after)

fun navBarToXml [t ::: Type] (m : mode t) = m

fun navToXml_build (n : navBar build) : xbody =
    navBarToXml' (printingNavBar n)

fun navToXml_print (n: navBar print) : xbody =
    navBarToXml' n

val emptyNavBar = NavBar ([], [])

fun mkNavItem text url =
    NavItem (text, url)

fun navAdd navItem navBar =
    case navBar of
        NavBar (before, []) => NavBar (navItem :: before, [])
      | NavBar (before, after) => NavBar (before, navItem :: after)

fun navAddActive navItem navBar =
    case navBar of
        NavBar (before, []) => NavBar (before, navItem :: [])
      | NavBar (before, after) => NavBar (List.append after before, navItem :: [])