0 | module Text.CSS.Selector

  2 | import Data.List

  3 | import Data.String

  4 | import Text.CSS.Class

  5 | import Text.CSS.Property

  6 | import Text.HTML.Tag

  8 | %default total

 10 | public export

 11 | data Combinator : Type where

 12 |   Descendant      : Combinator

 13 |   Child           : Combinator

 14 |   GeneralSibling  : Combinator

 15 |   AdjacentSibling : Combinator

 18 | Interpolation Combinator where

 19 |   interpolate Descendant      = ""

 20 |   interpolate Child           = ">"

 21 |   interpolate GeneralSibling  = "~"

 22 |   interpolate AdjacentSibling = "+"

 24 | public export

 25 | data AttributeValue : Type where

 26 |   Set      : AttributeValue

 27 |   Has      : String -> AttributeValue

 28 |   Equals   : String -> AttributeValue

 29 |   Contains : String -> AttributeValue

 30 |   Prefix   : String -> AttributeValue

 31 |   Suffix   : String -> AttributeValue

 34 | Interpolation AttributeValue where

 35 |   interpolate Set          = ""

 36 |   interpolate (Has s)      = "~=\{quote s}"

 37 |   interpolate (Equals s)   = "=\{quote s}"

 38 |   interpolate (Contains s) = "*=\{quote s}"

 39 |   interpolate (Prefix s)   = "^=\{quote s}"

 40 |   interpolate (Suffix s)   = "$=\{quote s}"

 42 | public export

 43 | data Selector : Type where

 44 |   Star    : Selector

 45 |   Id      : String -> Selector

 46 |   Class   : Class -> Selector

 47 |   Elem    : {str : _} -> (0 tag : HTMLTag str) -> Selector

 48 |   Attr    : String -> AttributeValue -> Selector

 49 |   Complex : Selector -> Combinator -> Selector -> Selector

 50 |   Nil     : Selector

 51 |   (::)    : Selector -> Selector -> Selector

 53 |   ||| Matches when the user activates (for example clicks on) an element.

 54 |   Active : Selector

 55 |   ||| Matches both the :link and :visited states of a link.

 56 |   AnyLink : Selector

 57 |   ||| Matches an <input> element whose input value is empty.

 58 |   Blank : Selector

 59 |   ||| Matches a radio button or checkbox in the selected state.

 60 |   Checked : Selector

 61 |   ||| Matches the element, or an ancestor of the element, that is currently being displayed.

 62 |   Current : Selector

 63 |   ||| Matches the one or more UI elements that are the default among a set of similar elements.

 64 |   Default : Selector

 65 |   ||| Select an element based on its directionality (value of the HTML dir attribute or CSS direction property).

 66 |   Dir : Direction -> Selector

 67 |   ||| Matches user interface elements that are in an disabled state.

 68 |   Disabled : Selector

 69 |   ||| Matches an element that has no children except optionally white space.

 70 |   Empty : Selector

 71 |   ||| Matches user interface elements that are in an enabled state.

 72 |   Enabled : Selector

 73 |   ||| In Paged Media, matches the first page.

 74 |   First : Selector

 75 |   ||| Matches an element that is first among its siblings.

 76 |   FirstChild : Selector

 77 |   ||| Matches an element which is first of a certain type among its siblings.

 78 |   FirstOfType : Selector

 79 |   ||| Matches when an element has focus.

 80 |   Focus : Selector

 81 |   ||| Matches when an element has focus and the focus should be visible to the user.

 82 |   FocusVisible : Selector

 83 |   ||| Matches an element with focus plus an element with a descendent that has focus.

 84 |   FocusWithin : Selector

 85 |   ||| Matches the elements after the current element.

 86 |   Future : Selector

 87 |   ||| Matches when the user hovers over an element.

 88 |   Hover : Selector

 89 |   ||| Matches UI elements whose value is in an indeterminate state, usually checkboxes.

 90 |   Indeterminate : Selector

 91 |   ||| Matches an element with a range when its value is in-range.

 92 |   InRange : Selector

 93 |   ||| Matches an element, such as an <input>, in an invalid state.

 94 |   Invalid : Selector

 95 |   ||| Matches an element based on language (value of the HTML lang attribute).

 96 |   Lang : String -> Selector

 97 |   ||| Matches an element which is last among its siblings.

 98 |   LastChild : Selector

 99 |   ||| Matches an element of a certain type that is last among its siblings.

100 |   LastOfType : Selector

101 |   ||| In Paged Media, matches left-hand pages.

102 |   Left : Selector

103 |   ||| Matches unvisited links.

104 |   Link : Selector

105 |   ||| Matches links pointing to pages that are in the same site as the current document.

106 |   LocalLink : Selector

107 |   |||Matches elements from a list of siblings — the siblings are matched by a formula of the form an+b (e.g. 2n + 1 would match elements 1, 3, 5, 7, etc. All the odd ones.)

108 |   NthChild : String -> Selector

109 |   |||Matches elements from a list of siblings — the siblings are matched by a formula of the form an+b (e.g. 2n + 1 would match elements 1, 3, 5, 7, etc. All the odd ones.)

110 |   NthOfType : String -> Selector

111 |   ||| Matches elements from a list of siblings, counting backwards from the end. The siblings are matched by a formula of the form an+b (e.g. 2n + 1 would match the last element in the sequence, then two elements before that, then two elements before that, etc. All the odd ones, counting from the end.)

112 |   NthLastChild : String -> Selector

113 |   ||| Matches elements from a list of siblings that are of a certain type (e.g. <p> elements), counting backwards from the end. The siblings are matched by a formula of the form an+b (e.g. 2n + 1 would match the last element of that type in the sequence, then two elements before that, then two elements before that, etc. All the odd ones, counting from the end.)

114 |   NthLastOfType : String -> Selector

115 |   ||| Matches an element that has no siblings.

116 |   OnlyChild : Selector

117 |   ||| Matches an element that is the only one of its type among its siblings.

118 |   OnlyOfType : Selector

119 |   ||| Matches form elements that are not required.

120 |   Optional : Selector

121 |   ||| Matches an element with a range when its value is out of range.

122 |   OutOfRange : Selector

123 |   ||| Matches the elements before the current element.

124 |   Past : Selector

125 |   ||| Matches an input element that is showing placeholder text.

126 |   PlaceholderShown : Selector

127 |   ||| Matches an element representing an audio, video, or similar resource that is capable of being “played” or “paused”, when that element is “playing”.

128 |   Playing : Selector

129 |   ||| Matches an element representing an audio, video, or similar resource that is capable of being “played” or “paused”, when that element is “paused”.

130 |   Paused : Selector

131 |   ||| Matches an element if it is not user-alterable.

132 |   ReadOnly : Selector

133 |   ||| Matches an element if it is user-alterable.

134 |   ReadWrite : Selector

135 |   ||| Matches form elements that are required.

136 |   Required : Selector

137 |   ||| In Paged Media, matches right-hand pages.

138 |   Right : Selector

139 |   ||| Matches an element that is the root of the document.

140 |   Root : Selector

141 |   ||| Matches any element that is a scope element.

142 |   Scope : Selector

143 |   ||| Matches an element such as an <input> element, in a valid state.

144 |   Valid : Selector

145 |   ||| Matches an element if it is the target of the current URL (i.e. if it has an ID matching the current URL fragment).

146 |   Target : Selector

147 |   ||| Matches visited links.

148 |   Visited : Selector

150 |   After : Selector

151 |   Backdrop : Selector

152 |   Before : Selector

153 |   Cue : Selector

154 |   CueRegion : Selector

155 |   FirstLetter : Selector

156 |   FirstLine : Selector

157 |   FileSelectorButton : Selector

158 |   Marker : Selector

159 |   Placeholder : Selector

160 |   Selection : Selector

164 | Interpolation Selector where

165 |   interpolate Star                        = "*"

166 |   interpolate (Id s)                      = "#\{s}"

167 |   interpolate (Class s)                   = ".\{s}"

168 |   interpolate (Elem {str} _)              = str

169 |   interpolate (Attr s v)                  = "[\{s}\{v}]"

170 |   interpolate []                          = ""

171 |   interpolate (h::t)                      = interpolate h ++ interpolate t

172 |   interpolate (Complex  s1 Descendant s2) = "\{s1} \{s2}"

173 |   interpolate (Complex  s1 c s2)          = "\{s1} \{c} \{s2}"

174 |   interpolate Active                      = ":active"

175 |   interpolate AnyLink                     = ":any-link"

176 |   interpolate Blank                       = ":blank"

177 |   interpolate Checked                     = ":checked"

178 |   interpolate Current                     = ":current"

179 |   interpolate Default                     = ":default"

180 |   interpolate (Dir x)                     = ":dir(\{x})"

181 |   interpolate Disabled                    = ":disabled"

182 |   interpolate Empty                       = ":empty"

183 |   interpolate Enabled                     = ":enabled"

184 |   interpolate First                       = ":first"

185 |   interpolate FirstChild                  = ":first-child"

186 |   interpolate FirstOfType                 = ":first-of-type"

187 |   interpolate Focus                       = ":focus"

188 |   interpolate FocusVisible                = ":focus-visible"

189 |   interpolate FocusWithin                 = ":focus-within"

190 |   interpolate Future                      = ":future"

191 |   interpolate Hover                       = ":hover"

192 |   interpolate Indeterminate               = ":indeterminate"

193 |   interpolate InRange                     = ":in-range"

194 |   interpolate Invalid                     = ":invalid"

195 |   interpolate (Lang x)                    = ":lang(\{x})"

196 |   interpolate LastChild                   = ":last-child"

197 |   interpolate LastOfType                  = ":last-of-type"

198 |   interpolate Left                        = ":left"

199 |   interpolate Link                        = ":link"

200 |   interpolate LocalLink                   = ":local-link"

201 |   interpolate (NthChild x)                = ":nth-child(\{x})"

202 |   interpolate (NthOfType x)               = ":nth-of-type(\#{x})"

203 |   interpolate (NthLastChild x)            = ":nth-last-child(\#{x})"

204 |   interpolate (NthLastOfType x)           = ":nth-last-of-type(\#{x})"

205 |   interpolate OnlyChild                   = ":only-child"

206 |   interpolate OnlyOfType                  = ":only-of-type"

207 |   interpolate Optional                    = ":optional"

208 |   interpolate OutOfRange                  = ":out-of-range"

209 |   interpolate Past                        = ":past"

210 |   interpolate PlaceholderShown            = ":placeholder-shown"

211 |   interpolate Playing                     = ":playing"

212 |   interpolate Paused                      = ":paused"

213 |   interpolate ReadOnly                    = ":read-only"

214 |   interpolate ReadWrite                   = ":read-write"

215 |   interpolate Required                    = ":required"

216 |   interpolate Right                       = ":right"

217 |   interpolate Root                        = ":root"

218 |   interpolate Scope                       = ":scope"

219 |   interpolate Valid                       = ":valid"

220 |   interpolate Target                      = ":target"

221 |   interpolate Visited                     = ":visited"

222 |   interpolate After                       = "::after"

223 |   interpolate Backdrop                    = "::backdrop"

224 |   interpolate Before                      = "::before"

225 |   interpolate Cue                         = "::cue"

226 |   interpolate CueRegion                   = "::cue-region"

227 |   interpolate FirstLetter                 = "::first-letter"

228 |   interpolate FirstLine                   = "::first-line"

229 |   interpolate FileSelectorButton          = "::file-selector-button"

230 |   interpolate Marker                      = "::marker"

231 |   interpolate Placeholder                 = "::placeholder"

232 |   interpolate Selection                   = "::selection"

234 | export %inline

235 | class : Class -> Selector

236 | class = Class

239 | classes : List Class -> Selector

240 | classes []        = []

241 | classes (x :: xs) = class x :: classes xs

243 | export %inline

244 | elem : {str : _} -> (0 tpe : HTMLTag str) -> Selector

245 | elem = Elem

248 | attribute : String -> Selector

249 | attribute s = Attr s Set

251 | export %inline

252 | id : String -> Selector

253 | id = Id