module FF.HTML.Spec.Common.Selector where
open import Agda.Builtin.String using (String)
open import Cubical.Data.Bool.Base using (Bool; false)
open import Cubical.Data.List.Base using (List; [])
import FF.HTML.Selector.Core as Selector
import FF.HTML.Selector.Semantics as Semantics
import FF.HTML.Spec.Common as Common
CompoundT : _
CompoundT = Selector.CompoundSelector Common.spec
ComplexT : _
ComplexT = Selector.ComplexSelector Common.spec
SelectorT : _
SelectorT = Selector.SelectorList Common.spec
TypedSimpleT : Common.TagName -> _
TypedSimpleT tagName = Selector.TypedSimple Common.spec tagName
UntypedSimpleT : _
UntypedSimpleT = Selector.UntypedSimple Common.spec
any : CompoundT
any = Selector.universal []
tag : Common.TagName -> CompoundT
tag tagName = Selector.typed tagName []
tagWith : (tagName : Common.TagName) -> List (TypedSimpleT tagName) -> CompoundT
tagWith = Selector.typed
idIs : String -> UntypedSimpleT
idIs = Selector.rawId
classContains : String -> UntypedSimpleT
classContains = Selector.rawClass
attrPresent : String -> UntypedSimpleT
attrPresent name = Selector.rawAttribute name Selector.rawPresent
attrEquals : String -> String -> UntypedSimpleT
attrEquals name value =
Selector.rawAttribute name
(Selector.rawMatch Selector.exact value Selector.documentCase)
noPseudo : Semantics.ElementContext Common.spec -> String -> Bool
noPseudo _ _ = false
noFunctionalPseudo :
Semantics.ElementContext Common.spec ->
String ->
String ->
Bool
noFunctionalPseudo _ _ _ = false
matcherWith : Semantics.TextDeciders -> Semantics.SelectorMatcher Common.spec
matcherWith text =
Semantics.matcherFromRenderer
Common.renderer
text
(\ keyName -> Semantics.sameText text keyName "id")
(\ keyName -> Semantics.sameText text keyName "class")
noPseudo
noFunctionalPseudo
matcher : Semantics.SelectorMatcher Common.spec
matcher = matcherWith Semantics.exactOnlyTextDeciders
render : SelectorT -> String
render = Selector.renderSelectorList Common.renderer
matchesRootWith : Semantics.TextDeciders -> SelectorT -> Common.HtmlT -> Bool
matchesRootWith text = Semantics.matchesRoot (matcherWith text)
matchesRoot : SelectorT -> Common.HtmlT -> Bool
matchesRoot = Semantics.matchesRoot matcher
selectWith : Semantics.TextDeciders -> SelectorT -> Common.HtmlT -> List Common.HtmlT
selectWith text = Semantics.select (matcherWith text)
select : SelectorT -> Common.HtmlT -> List Common.HtmlT
select = Semantics.select matcher