module FF.HTML.Spec.Safe.StyleSheet where open import Agda.Builtin.String using (String) open import Cubical.Data.Bool.Base using (Bool; false; true) open import Cubical.Data.List.Base using (List; []; _∷_) import FF.CSS.Spec.Common as CommonCSS import FF.CSS.Spec.Loose as LooseCSS import FF.CSS.Spec.Safe as CSS import FF.CSS.Spec.Safe.Syntax as CSSSyntax import FF.HTML.Spec.Common as CommonHTML import FF.HTML.Spec.Loose as LooseHTML import FF.HTML.Spec.Safe as HTML import FF.HTML.Spec.Safe.Selector as Selector import FF.HTML.StyleSheet.Core as Sheet RuleT : _ RuleT = Sheet.StyleRule HTML.spec CSS.spec StyleSheetT : _ StyleSheetT = Sheet.StyleSheet HTML.spec CSS.spec MatchedRuleT : _ MatchedRuleT = Sheet.MatchedRule HTML.spec CSS.spec ElementStyleT : _ ElementStyleT = Sheet.ElementStyle HTML.spec CSS.spec rule : Selector.SelectorT -> List CSS.DeclarationT -> RuleT rule = Sheet.styleRule sheet : List RuleT -> StyleSheetT sheet = Sheet.fromRules declaration : (propertyName : CSS.PropertyName) -> CSS.CssValue propertyName -> CSS.DeclarationT declaration = CSS.declaration render : StyleSheetT -> String render = Sheet.renderStyleSheet HTML.renderer CSS.renderer toCommon : StyleSheetT -> Sheet.StyleSheet CommonHTML.spec CommonCSS.spec toCommon = Sheet.mapStyleSheet HTML.toCommon CSS.toCommon toLoose : StyleSheetT -> Sheet.StyleSheet LooseHTML.spec LooseCSS.spec toLoose = Sheet.mapStyleSheet HTML.toLoose CSS.toLoose renderedByCommonRenderer : StyleSheetT -> String renderedByCommonRenderer stylesheet = Sheet.renderStyleSheet CommonHTML.renderer CommonCSS.renderer (toCommon stylesheet) renderedByLooseRenderer : StyleSheetT -> String renderedByLooseRenderer stylesheet = Sheet.renderStyleSheet LooseHTML.renderer LooseCSS.renderer (toLoose stylesheet) matchingRules : StyleSheetT -> HTML.HtmlT -> List MatchedRuleT matchingRules = Sheet.matchingStyleSheet Selector.matcher styledElements : StyleSheetT -> HTML.HtmlT -> List ElementStyleT styledElements = Sheet.styledElements Selector.matcher hasMatchingRules : StyleSheetT -> HTML.HtmlT -> Bool hasMatchingRules stylesheet html with matchingRules stylesheet html ... | [] = false ... | _ ∷ _ = true styleElement : StyleSheetT -> HTML.HtmlT styleElement stylesheet = HTML.element HTML.styleTag [] (HTML.text (render stylesheet) ∷ []) css : (propertyName : CSS.PropertyName) -> CSS.CssValue propertyName -> CSS.DeclarationT css = CSSSyntax._:=_