annotate datebox.ur @ 5:4385bc6a0d2d

Some Datebox functions related to dates
author Adam Chlipala <adam@chlipala.net>
date Thu, 10 Feb 2011 12:39:20 -0500
parents 377c11586999
children bbdedfde154e
rev   line source
adam@2 1 style calendar
adam@2 2 style prev
adam@2 3 style this
adam@2 4 style next
adam@2 5 style weekday
adam@2 6 style curday
adam@2 7 style otherday
adam@4 8 style selday
adam@2 9
adam@2 10 datatype month = Prev | This | Next
adam@2 11
adam@4 12 type date = {Year : int, Month : int, Day : int}
adam@5 13 val date_ord = mkOrd {Lt = fn {Year = y1, Month = m1, Day = d1} {Year = y2, Month = m2, Day = d2} =>
adam@5 14 y1 < y2 || (y1 = y2 && m1 < m2) || (y1 = y2 && m1 = m2 && d1 < d2),
adam@5 15 Le = fn {Year = y1, Month = m1, Day = d1} {Year = y2, Month = m2, Day = d2} =>
adam@5 16 y1 < y2 || (y1 = y2 && m1 < m2) || (y1 = y2 && m1 = m2 && d1 <= d2)}
adam@4 17
adam@2 18 type t = {Month : source {ThisMonth : int, Year : int,
adam@2 19 ThisMonthLength : int, PrevMonthLength : int,
adam@2 20 MondayMonth : month, MondayDay : int,
adam@2 21 PrevMonthName : string, ThisMonthName : string, NextMonthName : string},
adam@4 22 Day : source date,
adam@4 23 Hide : source bool}
adam@2 24
adam@2 25 fun pad len n =
adam@2 26 let
adam@2 27 val s = show n
adam@2 28
adam@2 29 fun pad' len s =
adam@2 30 if len <= 0 then
adam@2 31 s
adam@2 32 else
adam@2 33 pad' (len-1) ("0" ^ s)
adam@2 34 in
adam@2 35 pad' (len - String.length s) s
adam@2 36 end
adam@2 37
adam@5 38 fun time {Year = y, Month = m, Day = d} = readError (show y ^ "-" ^ pad 2 m ^ "-" ^ pad 2 d ^ " 00:00:00")
adam@5 39
adam@2 40 fun monthLen m =
adam@2 41 let
adam@2 42 fun f n tm =
adam@2 43 let
adam@2 44 val next = addSeconds tm (60 * 60 * 24)
adam@2 45 val nextMon = readError (timef "%m" next)
adam@2 46 in
adam@2 47 if nextMon = m.Month then
adam@2 48 f (n+1) next
adam@2 49 else
adam@2 50 n
adam@2 51 end
adam@2 52 in
adam@2 53 f 28 (readError (show m.Year ^ "-" ^ pad 2 m.Month ^ "-28 00:00:00"))
adam@2 54 end
adam@2 55
adam@2 56 fun weekdayToNum s =
adam@2 57 case s of
adam@2 58 "Mon" => 0
adam@2 59 | "Tue" => 1
adam@2 60 | "Wed" => 2
adam@2 61 | "Thu" => 3
adam@2 62 | "Fri" => 4
adam@2 63 | "Sat" => 5
adam@2 64 | "Sun" => 6
adam@2 65 | _ => error <xml>Datebox: Bad weekday name</xml>
adam@2 66
adam@2 67 fun timeOfMonth my =
adam@2 68 readError (show my.Year ^ "-" ^ pad 2 my.Month ^ "-01 00:00:00")
adam@2 69
adam@3 70 fun monthInfo' this =
adam@2 71 let
adam@2 72 val prev = if this.Month = 1 then
adam@2 73 {Month = 12, Year = this.Year - 1}
adam@2 74 else
adam@2 75 {Month = this.Month-1, Year = this.Year}
adam@2 76 val prevLen = monthLen prev
adam@2 77
adam@2 78 val next = if this.Month = 12 then
adam@2 79 {Month = 1, Year = this.Year + 1}
adam@2 80 else
adam@2 81 {Month = this.Month + 1, Year = this.Year}
adam@2 82
adam@2 83 val firstDow = weekdayToNum (timef "%a" (timeOfMonth this))
adam@2 84 in
adam@2 85 {ThisMonth = this.Month, Year = this.Year,
adam@2 86 ThisMonthLength = monthLen this,
adam@2 87 PrevMonthLength = prevLen,
adam@2 88 MondayMonth = if firstDow = 0 then This else Prev,
adam@2 89 MondayDay = if firstDow = 0 then 1 else prevLen - (firstDow - 1),
adam@2 90 PrevMonthName = timef "%b" (timeOfMonth prev),
adam@2 91 ThisMonthName = timef "%b" (timeOfMonth this),
adam@2 92 NextMonthName = timef "%b" (timeOfMonth next)}
adam@2 93 end
adam@2 94
adam@3 95 fun monthInfo this = return (monthInfo' this)
adam@3 96
adam@4 97 fun create tm =
adam@2 98 year <- return (readError (timef "%Y" tm));
adam@2 99 month <- return (readError (timef "%m" tm));
adam@4 100 minf <- source (monthInfo' {Month = month, Year = year});
adam@2 101 day <- return (readError (timef "%d" tm));
adam@4 102 day <- source {Year = year, Month = month, Day = day};
adam@4 103 hide <- source True;
adam@4 104 return {Month = minf, Day = day, Hide = hide}
adam@2 105
adam@4 106 fun render' t =
adam@4 107 minf <- signal t.Month;
adam@4 108 let
adam@4 109 fun rows year month day =
adam@4 110 let
adam@4 111 fun row year month day weekday =
adam@4 112 if weekday >= 7 then
adam@4 113 <xml/>
adam@4 114 else
adam@4 115 <xml>
adam@4 116 <dyn signal={let
adam@4 117 val thisDate = {Year = year,
adam@4 118 Month = case month of
adam@4 119 Prev => if minf.ThisMonth = 1 then 12 else minf.ThisMonth - 1
adam@4 120 | This => minf.ThisMonth
adam@4 121 | Next => if minf.ThisMonth = 12 then 1 else minf.ThisMonth + 1,
adam@4 122 Day = day}
adam@4 123 in
adam@4 124 cday <- signal t.Day;
adam@4 125 return (if Record.equal thisDate cday then
adam@4 126 <xml><td class={selday}>{[day]}</td></xml>
adam@4 127 else case month of
adam@4 128 This => <xml><td class={curday}
adam@4 129 onclick={set t.Day thisDate}>{[day]}</td></xml>
adam@4 130 | _ => <xml><td class={otherday}>{[day]}</td></xml>)
adam@4 131 end}/>
adam@4 132 {let
adam@4 133 val (year, month, day) =
adam@4 134 case month of
adam@4 135 Prev => if day = minf.PrevMonthLength then
adam@4 136 (if minf.ThisMonth = 1 then year + 1 else year, This, 1)
adam@4 137 else
adam@4 138 (year, Prev, day+1)
adam@4 139 | This => if day = minf.ThisMonthLength then
adam@4 140 (if minf.ThisMonth = 12 then year + 1 else year, Next, 1)
adam@4 141 else
adam@4 142 (year, This, day+1)
adam@4 143 | Next => (year, Next, day+1)
adam@4 144 in
adam@4 145 row year month day (weekday+1)
adam@4 146 end}
adam@4 147 </xml>
adam@4 148 in
adam@4 149 case month of
adam@4 150 Next => <xml/>
adam@4 151 | _ =>
adam@4 152 <xml>
adam@4 153 <tr>{row year month day 0}</tr>
adam@4 154 {let
adam@4 155 val next =
adam@4 156 case month of
adam@4 157 Prev => Some (if minf.ThisMonth = 1 then year + 1 else year, This, day + 7 - minf.PrevMonthLength)
adam@4 158 | This =>
adam@4 159 Some (if day + 7 > minf.ThisMonthLength then
adam@4 160 (if minf.ThisMonth = 12 then year + 1 else year, Next, day + 7 - minf.ThisMonthLength)
adam@4 161 else
adam@4 162 (year, This, day + 7))
adam@4 163 | Next => None
adam@2 164 in
adam@4 165 case next of
adam@4 166 None => <xml/>
adam@4 167 | Some (year, month, day) => rows year month day
adam@4 168 end}
adam@4 169 </xml>
adam@4 170 end
adam@4 171 in
adam@4 172 return <xml>
adam@4 173 <table class={calendar}>
adam@4 174 <tr>
adam@4 175 <th class={prev} colspan={2}
adam@4 176 onclick={minf <- rpc (monthInfo (if minf.ThisMonth = 1 then
adam@4 177 {Month = 12, Year = minf.Year - 1}
adam@4 178 else
adam@4 179 {Month = minf.ThisMonth - 1, Year = minf.Year}));
adam@4 180 set t.Month minf}>&lt;&lt; {[minf.PrevMonthName]}</th>
adam@4 181 <th class={this} colspan={3}>{[minf.ThisMonthName]} {[minf.Year]}</th>
adam@4 182 <th class={next} colspan={2}
adam@4 183 onclick={minf <- rpc (monthInfo (if minf.ThisMonth = 12 then
adam@4 184 {Month = 1, Year = minf.Year + 1}
adam@4 185 else
adam@4 186 {Month = minf.ThisMonth + 1, Year = minf.Year}));
adam@4 187 set t.Month minf}>{[minf.NextMonthName]} >></th>
adam@4 188 </tr>
adam@4 189 <tr class={weekday}> <th>M</th> <th>Tu</th> <th>W</th> <th>Th</th> <th>F</th> <th>Sa</th> <th>Su</th> </tr>
adam@4 190 {rows (if minf.ThisMonth = 1 && (case minf.MondayMonth of This => False | _ => True) then
adam@4 191 minf.Year - 1
adam@4 192 else
adam@4 193 minf.Year) minf.MondayMonth minf.MondayDay}
adam@4 194 </table>
adam@4 195 </xml>
adam@4 196 end
adam@2 197
adam@4 198 fun render t = <xml>
adam@4 199 <dyn signal={date <- signal t.Day;
adam@4 200 return <xml>{[date.Year]}-{[date.Month]}-{[date.Day]}</xml>}/>
adam@4 201 <dyn signal={hd <- signal t.Hide;
adam@4 202 if hd then
adam@4 203 return <xml><button value="Choose" onclick={set t.Hide False}/></xml>
adam@4 204 else
adam@4 205 main <- render' t;
adam@4 206 return <xml><button value="Hide" onclick={set t.Hide True}/><br/>{main}</xml>}/>
adam@4 207 </xml>
adam@4 208
adam@4 209 fun value t = signal t.Day