HTML.Showcase

module HTML.Showcase where

open import Agda.Builtin.String using (String)
open import Cubical.Data.Bool.Base using (true; false)
open import Cubical.Data.List.Base using ([]; _∷_)
import FF.CSS.Spec.Safe.Syntax as CSS

open import FF.HTML.Render using (render)
import FF.HTML.Spec.Safe.Selector as Select
import FF.HTML.Spec.Safe.StyleSheet as StyleSheet
open import FF.HTML.Spec.Safe.Syntax

infixr 5 _∷ˢ_

_∷ˢ_ : CSS.DeclarationT -> InlineStyle -> InlineStyle
_∷ˢ_ = styleCons

rem : String -> CSS.LengthPercentage
rem value = CSS.lp (CSS.remLength value)

px : String -> CSS.LengthPercentage
px value = CSS.lp (CSS.pxLength value)

percent : String -> CSS.LengthPercentage
percent value = CSS.pct (CSS.percent value)

size-rem : String -> CSS.PreferredSize
size-rem value = CSS.size-lp (rem value)

size-percent : String -> CSS.PreferredSize
size-percent value = CSS.size-lp (percent value)

margin-rem : String -> CSS.MarginSize
margin-rem value = CSS.margin-lp (rem value)

color-hex : String -> CSS.Color
color-hex value = CSS.hex (CSS.hexColor value)

custom-property : String -> String -> CSS.DeclarationT
custom-property name value =
  CSS._:=_ (CSS.customProp name) (CSS.specific (CSS.customValue (CSS.raw value)))

bodyStyle : InlineStyle
bodyStyle =
  custom-property "brand" "#195a96" ∷ˢ
  custom-property "accent" "#df7b36" ∷ˢ
  custom-property "surface" "#ffffff" ∷ˢ
  CSS.background-color (color-hex "#f4f7fb") ∷ˢ
  CSS.color (color-hex "#172033") ∷ˢ
  CSS.margin (CSS.oneSide CSS.marginAuto) ∷ˢ
  CSS.font-size (rem "1") ∷ˢ
  styleOne (CSS._:=_ CSS.boxSizingProp (CSS.specific (CSS.boxSizingValue CSS.borderBox)))

shellStyle : InlineStyle
shellStyle =
  CSS.width (size-percent "100") ∷ˢ
  CSS.margin (CSS.twoSides (margin-rem "0") (margin-rem "0")) ∷ˢ
  CSS.padding (CSS.twoSides (rem "2") (rem "2.5")) ∷ˢ
  styleOne (CSS._:=_ CSS.maxWidthProp (CSS.specific (CSS.maxWidthValue (CSS.maxSize (CSS.sizeLengthPercentage (rem "86"))))))

barStyle : InlineStyle
barStyle =
  CSS.display (CSS.displayOutsideInside CSS.outsideBlock CSS.insideFlex) ∷ˢ
  CSS.gap (CSS.oneValue (CSS.gap-value (rem "1"))) ∷ˢ
  CSS.padding (CSS.twoSides (rem "1") (rem "1.25")) ∷ˢ
  CSS.background-color (color-hex "#ffffff") ∷ˢ
  styleOne (CSS._:=_ CSS.borderRadiusProp (CSS.specific (CSS.borderRadiusValue (CSS.radiusSimple (CSS.oneSide (rem "1"))))))

heroStyle : InlineStyle
heroStyle =
  CSS.display (CSS.displayOutsideInside CSS.outsideBlock CSS.insideGrid) ∷ˢ
  CSS.gap (CSS.oneValue (CSS.gap-value (rem "1.5"))) ∷ˢ
  CSS.padding (CSS.twoSides (rem "3") (rem "2.5")) ∷ˢ
  CSS.background-color (color-hex "#e7f0ff") ∷ˢ
  styleOne (CSS._:=_ CSS.borderRadiusProp (CSS.specific (CSS.borderRadiusValue (CSS.radiusSimple (CSS.oneSide (rem "1.25"))))))

cardStyle : InlineStyle
cardStyle =
  CSS.background-color (color-hex "#ffffff") ∷ˢ
  CSS.padding (CSS.oneSide (rem "1.25")) ∷ˢ
  CSS.display (CSS.displayOutsideInside CSS.outsideBlock CSS.insideGrid) ∷ˢ
  CSS.gap (CSS.oneValue (CSS.gap-value (rem "0.5"))) ∷ˢ
  styleOne (CSS._:=_ CSS.borderRadiusProp (CSS.specific (CSS.borderRadiusValue (CSS.radiusSimple (CSS.oneSide (rem "0.75"))))))

mutedStyle : InlineStyle
mutedStyle =
  CSS.color (color-hex "#5f6c80") ∷ˢ
  styleOne (CSS.font-size (rem "0.95"))

sectionStyle : InlineStyle
sectionStyle =
  CSS.display (CSS.displayOutsideInside CSS.outsideBlock CSS.insideGrid) ∷ˢ
  CSS.gap (CSS.oneValue (CSS.gap-value (rem "1"))) ∷ˢ
  CSS.margin (CSS.twoSides (margin-rem "2") (margin-rem "0")) ∷ˢ
  styleOne (CSS.padding (CSS.twoSides (rem "1.5") (rem "0")))

controlStyle : InlineStyle
controlStyle =
  CSS.width (size-percent "100") ∷ˢ
  CSS.padding (CSS.twoSides (rem "0.75") (rem "0.85")) ∷ˢ
  styleOne (CSS._:=_ CSS.borderRadiusProp (CSS.specific (CSS.borderRadiusValue (CSS.radiusSimple (CSS.oneSide (rem "0.5"))))))

buttonStyle : InlineStyle
buttonStyle =
  CSS.background-color (color-hex "#195a96") ∷ˢ
  CSS.color (color-hex "#ffffff") ∷ˢ
  CSS.padding (CSS.twoSides (rem "0.75") (rem "1")) ∷ˢ
  styleOne (CSS._:=_ CSS.borderRadiusProp (CSS.specific (CSS.borderRadiusValue (CSS.radiusSimple (CSS.oneSide (rem "0.5"))))))

dashboardCss : String
dashboardCss =
  ".topbar{justify-content:space-between;align-items:center;box-shadow:0 18px 45px rgba(25,90,150,.12)}"
  ++ ".nav-list{display:flex;gap:1rem;list-style:none;margin:0;padding:0}"
  ++ ".hero{grid-template-columns:minmax(0,1.15fr) minmax(18rem,.85fr);align-items:center}"
  ++ ".metrics{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:1rem}"
  ++ ".two-col{display:grid;grid-template-columns:minmax(0,1fr) minmax(18rem,.8fr);gap:1rem}"
  ++ ".field{display:grid;gap:.35rem;margin-block:.75rem}"
  ++ "table{width:100%;border-collapse:collapse;background:#fff}"
  ++ "th,td{padding:.75rem;border-bottom:1px solid #d9e2ef;text-align:left}"
  ++ "img,video,iframe{max-width:100%;border-radius:.75rem}"

exampleStyleSheet : StyleSheet.StyleSheetT
exampleStyleSheet =
  StyleSheet.sheet
    ( StyleSheet.rule
        (Select.single (Select.compound (Select.tag bodyTag)))
        ( CSS.background-color (color-hex "#f4f7fb")
        ∷ CSS.color (color-hex "#172033")
        ∷ CSS.margin (CSS.oneSide CSS.marginAuto)
        ∷ []
        )
    ∷ StyleSheet.rule
        (Select.single (Select.compound (Select.tagWith sectionTag (Select.dataAttrEquals "stage" "stylesheet" ∷ []))))
        ( CSS.display (CSS.displayOutsideInside CSS.outsideBlock CSS.insideGrid)
        ∷ CSS.gap (CSS.oneValue (CSS.gap-value (rem "1")))
        ∷ CSS.padding (CSS.twoSides (rem "1.5") (rem "1.5"))
        ∷ CSS.background-color (color-hex "#ffffff")
        ∷ []
        )
    ∷ StyleSheet.rule
        (Select.single
          (Select.descendantOf
            (Select.compound (Select.tag navTag))
            (Select.tagWith aTag (Select.typedClass "nav-link" ∷ []))))
        ( CSS.color (CSS.named CSS.rebeccapurple)
        ∷ CSS.font-size (rem "1.05")
        ∷ []
        )
    ∷ StyleSheet.rule
        (Select.single (Select.compound (Select.tagWith pTag (Select.typedPseudo "empty" ∷ []))))
        (CSS.display (CSS.displayBox CSS.displayNone) ∷ [])
    ∷ []
    )

exampleStyleSheetText : String
exampleStyleSheetText = StyleSheet.render exampleStyleSheet

headWithTitle : String -> HtmlT
headWithTitle titleText =
  ‹ head ›
    void Feature.voidMeta (meta-charset "utf-8" ∷ []) ∷
    void Feature.voidMeta
      ( meta-name "viewport"
      ∷ meta-content "width=device-width, initial-scale=1"
      ∷ []
      )
    ∷
    void Feature.voidMeta
      ( meta-name "theme-color"
      ∷ meta-content "#195a96"
      ∷ []
      )
    ∷
    ‹ title-tag ›
      text titleText ∷ []
    ‹/› ∷
    void Feature.voidLink
      ( link-rel-keywords (relCons relPreload (relOne relStylesheet))
      ∷ link-href "/assets/console.css"
      ∷ link-as asStyle
      ∷ link-type "text/css"
      ∷ link-fetchpriority high
      ∷ []
      )
    ∷
    ‹ styleTag ›
      text dashboardCss ∷ []
    ‹/› ∷
    []
  ‹/›

documentHead : HtmlT
documentHead = headWithTitle "Safe HTML Operations Console"

introPage : HtmlT
introPage =
  ‹ html ❴ attribute langAttr (language "en") ∷ [] ❵›
    headWithTitle "ff-html intro example" ∷
    ‹ body ❴ style-decls bodyStyle ∷ data- "example" "intro" ∷ [] ❵›
      ‹ main ❴ style-decls shellStyle ∷ [] ❵›
        ‹ h1 › text "Intro: typed nodes and attributes" ∷ [] ‹/› ∷
        ‹ p ❴ style-decls mutedStyle ∷ [] ❵›
          text "This smallest page uses safe tags, global attributes, typed language metadata, and ff-css inline declarations." ∷ []
        ‹/› ∷
        ‹ a ❴ href "https://developer.mozilla.org/en-US/docs/Web/HTML"
              ∷ target blank
              ∷ rel-keywords (relCons relExternal (relCons relNoopener (relOne relNoreferrer)))
              ∷ style-decls buttonStyle
              ∷ [] ❵›
          text "Open HTML reference" ∷ []
        ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

semanticArticlePage : HtmlT
semanticArticlePage =
  ‹ html ❴ attribute langAttr (language "en") ∷ [] ❵›
    headWithTitle "ff-html semantic article example" ∷
    ‹ body ❴ style-decls bodyStyle ∷ data- "example" "semantic-article" ∷ [] ❵›
      ‹ main ❴ style-decls shellStyle ∷ [] ❵›
        ‹ articleTag ❴ class "article-example"
                     ∷ attribute itemtypeAttr "https://schema.org/TechArticle"
                     ∷ attribute itemscopeAttr present
                     ∷ style-decls cardStyle
                     ∷ [] ❵›
          ‹ header ›
            ‹ h1 ❴ attribute itempropAttr (tokens "headline") ∷ [] ❵›
              text "Semantic article with typed Safe attributes" ∷ []
            ‹/› ∷
            ‹ p ❴ style-decls mutedStyle ∷ [] ❵›
              text "Published " ∷
              ‹ timeTag ❴ attribute (datetimeAttr datetimeTime) (dateTime "2026-06-14")
                         ∷ attribute itempropAttr (tokens "datePublished")
                         ∷ [] ❵›
                text "14 June 2026" ∷ []
              ‹/› ∷
              text "." ∷
              []
            ‹/› ∷
            []
          ‹/› ∷
          ‹ p ›
            text "The example mixes " ∷
            ‹ codeTag › text "code" ∷ [] ‹/› ∷
            text ", " ∷
            ‹ kbdTag › text "keyboard" ∷ [] ‹/› ∷
            text ", " ∷
            ‹ markTag › text "highlighted" ∷ [] ‹/› ∷
            text ", and quoted inline text." ∷
            []
          ‹/› ∷
          ‹ blockquoteTag ❴ attribute (citeAttr citeBlockquote) (url "https://developer.mozilla.org/en-US/docs/Web/HTML")
                         ∷ [] ❵›
            ‹ p ›
              text "HTML semantics are represented as ordinary typed values before rendering." ∷ []
            ‹/› ∷
            []
          ‹/› ∷
          ‹ olTag ❴ attribute startAttr "3"
                  ∷ attribute olTypeAttr upperRoman
                  ∷ [] ❵›
            ‹ li › text "Construct a typed tree." ∷ [] ‹/› ∷
            ‹ li › text "Render it with an explicit renderer." ∷ [] ‹/› ∷
            ‹ li › text "Check selectors and stylesheets over the same tree." ∷ [] ‹/› ∷
            []
          ‹/› ∷
          ‹ p ›
            ‹ delTag ❴ attribute (datetimeAttr datetimeDel) (dateTime "2026-06-01")
                      ∷ attribute (citeAttr citeDel) (url "/notes/old")
                      ∷ [] ❵›
              text "Old wording" ∷ []
            ‹/› ∷
            text " was replaced by " ∷
            ‹ insTag ❴ attribute (datetimeAttr datetimeIns) (dateTime "2026-06-14")
                      ∷ attribute (citeAttr citeIns) (url "/notes/current")
                      ∷ [] ❵›
              text "current wording" ∷ []
            ‹/› ∷
            text "." ∷
            []
          ‹/› ∷
          []
        ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

selectorStyleSheetPage : HtmlT
selectorStyleSheetPage =
  ‹ html ❴ attribute langAttr (language "en") ∷ [] ❵›
    headWithTitle "ff-html selector stylesheet example" ∷
    ‹ body ❴ data- "example" "selectors-and-stylesheets" ∷ [] ❵›
      StyleSheet.styleElement exampleStyleSheet ∷
      ‹ main ❴ class "shell" ∷ [] ❵›
        ‹ h1 › text "Selectors and stylesheets" ∷ [] ‹/› ∷
        ‹ nav ❴ aria- "label" "Example sections" ∷ [] ❵›
          ‹ a ❴ href "#styled"
                ∷ class "nav-link"
                ∷ rel-keyword relBookmark
                ∷ [] ❵›
            text "Styled section" ∷ []
          ‹/› ∷
          []
        ‹/› ∷
        ‹ section ❴ id "styled" ∷ data- "stage" "stylesheet" ∷ [] ❵›
          ‹ h2 › text "Matched by a typed data-* selector" ∷ [] ‹/› ∷
          ‹ p › text "The stylesheet on this page is built from Safe selectors and ff-css declarations." ∷ [] ‹/› ∷
          ‹ p › [] ‹/› ∷
          []
        ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

topBar : HtmlT
topBar =
  ‹ header ❴ class "topbar" ∷ style-decls barStyle ∷ [] ❵›
    ‹ div ❴ class "brand" ∷ [] ❵›
      ‹ h1 ❴ style-decls (CSS.margin (CSS.oneSide (margin-rem "0")) ∷ˢ styleOne (CSS.font-size (rem "1.25"))) ∷ [] ❵›
        text "Operations Console" ∷ []
      ‹/› ∷
      ‹ p ❴ style-decls mutedStyle ∷ [] ❵›
        text "Typed HTML composed from the Safe spec and CSS declarations." ∷ []
      ‹/› ∷
      []
    ‹/› ∷
    ‹ nav ❴ aria- "label" "Primary" ∷ [] ❵›
      ‹ ul ❴ class "nav-list" ∷ [] ❵›
        ‹ li › ‹ a ❴ href "#metrics" ∷ rel-keyword relBookmark ∷ [] ❵› text "Metrics" ∷ [] ‹/› ∷ [] ‹/› ∷
        ‹ li › ‹ a ❴ href "#intake" ∷ rel-keyword relBookmark ∷ [] ❵› text "Intake" ∷ [] ‹/› ∷ [] ‹/› ∷
        ‹ li › ‹ a ❴ href "#media" ∷ rel-keyword relBookmark ∷ [] ❵› text "Media" ∷ [] ‹/› ∷ [] ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

hero : HtmlT
hero =
  ‹ section ❴ class "hero" ∷ style-decls heroStyle ∷ aria- "labelledby" "hero-title" ∷ [] ❵›
    ‹ div ›
      ‹ h1 ❴ id "hero-title" ∷ [] ❵›
        text "A non-trivial page rendered from typed Agda data" ∷ []
      ‹/› ∷
      ‹ p ❴ style-decls mutedStyle ∷ [] ❵›
        text "The document uses indexed HTML attributes, typed token lists, and inline CSS declarations imported from ff-css." ∷ []
      ‹/› ∷
      ‹ a ❴ href "https://developer.mozilla.org/en-US/docs/Web/HTML"
            ∷ target blank
            ∷ rel-keywords (relCons relExternal (relCons relNoopener (relOne relNoreferrer)))
            ∷ style-decls buttonStyle
            ∷ [] ❵›
        text "Open MDN HTML reference" ∷ []
      ‹/› ∷
      []
    ‹/› ∷
    ‹ figureTag ❴ style-decls cardStyle ∷ [] ❵›
      void Feature.voidImg
        ( src "/assets/typed-console.png"
        ∷ alt "Dashboard mockup with charts and form controls"
        ∷ img-loading eager
        ∷ img-fetchpriority high
        ∷ []
        )
      ∷
      ‹ figcaptionTag ❴ style-decls mutedStyle ∷ [] ❵›
        text "The image element is represented as a void element with typed media attributes." ∷ []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

metricCard : String -> String -> String -> HtmlT
metricCard label value detail =
  ‹ articleTag ❴ class "metric-card" ∷ style-decls cardStyle ∷ [] ❵›
    ‹ span ❴ style-decls mutedStyle ∷ [] ❵› text label ∷ [] ‹/› ∷
    ‹ strongTag ❴ style-decls (CSS.font-size (rem "1.8") ∷ˢ styleOne (CSS.color (color-hex "#195a96"))) ∷ [] ❵›
      text value ∷ []
    ‹/› ∷
    ‹ p ❴ style-decls mutedStyle ∷ [] ❵› text detail ∷ [] ‹/› ∷
    []
  ‹/›

metrics : HtmlT
metrics =
  ‹ section ❴ id "metrics" ∷ style-decls sectionStyle ∷ aria- "labelledby" "metrics-title" ∷ [] ❵›
    ‹ h2 ❴ id "metrics-title" ∷ [] ❵› text "Coverage snapshot" ∷ [] ‹/› ∷
    ‹ div ❴ class "metrics" ∷ [] ❵›
      metricCard "Tags" "115" "Active HTML elements represented." ∷
      metricCard "Attributes" "126" "MDN table names covered by renderers." ∷
      metricCard "Token grammars" "3" "rel, sandbox, and controlslist are typed." ∷
      metricCard "CSS source" "ff-css" "Inline style declarations come from the CSS library." ∷
      []
    ‹/› ∷
    []
  ‹/›

reportTable : HtmlT
reportTable =
  ‹ section ❴ style-decls sectionStyle ∷ [] ❵›
    ‹ h2 › text "Recent formalisation work" ∷ [] ‹/› ∷
    ‹ table ❴ table-summary "Summary of represented HTML areas" ∷ [] ❵›
      ‹ caption ❴ legacy-align alignCaption "top" ∷ [] ❵›
        text "HTML Safe coverage ledger" ∷ []
      ‹/› ∷
      ‹ theadTag ›
        ‹ tr ›
          ‹ th ❴ th-abbr "Area" ∷ [] ❵› text "Area" ∷ [] ‹/› ∷
          ‹ th ❴ th-abbr "Status" ∷ [] ❵› text "Status" ∷ [] ‹/› ∷
          ‹ th ❴ th-abbr "Notes" ∷ [] ❵› text "Notes" ∷ [] ‹/› ∷
          []
        ‹/› ∷
        []
      ‹/› ∷
      ‹ tbody ›
        ‹ tr ›
          ‹ td › text "Elements" ∷ [] ‹/› ∷
          ‹ td › text "Done" ∷ [] ‹/› ∷
          ‹ td › text "All active MDN groups are represented." ∷ [] ‹/› ∷
          []
        ‹/› ∷
        ‹ tr ›
          ‹ td › text "Attributes" ∷ [] ‹/› ∷
          ‹ td › text "Broad partial" ∷ [] ‹/› ∷
          ‹ td › text "Names and rendering are covered; deeper constraints continue to grow." ∷ [] ‹/› ∷
          []
        ‹/› ∷
        ‹ tr ›
          ‹ td › text "CSS integration" ∷ [] ‹/› ∷
          ‹ td › text "Started" ∷ [] ‹/› ∷
          ‹ td › text "style accepts ff-css declarations through InlineStyle." ∷ [] ‹/› ∷
          []
        ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

intakeForm : HtmlT
intakeForm =
  ‹ section ❴ id "intake" ∷ class "two-col" ∷ style-decls sectionStyle ∷ [] ❵›
    ‹ form ❴ action "/requests"
            ∷ method post
            ∷ form-autocomplete autocompleteOn
            ∷ accept-charset "UTF-8"
            ∷ style-decls cardStyle
            ∷ [] ❵›
      ‹ h2 › text "Request intake" ∷ [] ‹/› ∷
      ‹ label ❴ for "requester" ∷ class "field" ∷ [] ❵›
        text "Requester email" ∷
        void Feature.voidInput
          ( input-type emailInput
          ∷ input-name "requester"
          ∷ id "requester"
          ∷ placeholder "[email protected]"
          ∷ input-autocomplete (autocompleteTokens "email")
          ∷ style-decls controlStyle
          ∷ required
          ∷ []
          )
        ∷ []
      ‹/› ∷
      ‹ label ❴ for "plan" ∷ class "field" ∷ [] ❵›
        text "Plan" ∷
        ‹ select ❴ id "plan"
                 ∷ select-required
                 ∷ select-autocomplete autocompleteOff
                 ∷ style-decls controlStyle
                 ∷ [] ❵›
          ‹ option › text "Starter" ∷ [] ‹/› ∷
          ‹ option › text "Team" ∷ [] ‹/› ∷
          ‹ option › text "Enterprise" ∷ [] ‹/› ∷
          []
        ‹/› ∷
        []
      ‹/› ∷
      ‹ label ❴ for "notes" ∷ class "field" ∷ [] ❵›
        text "Notes" ∷
        ‹ textarea ❴ id "notes"
                    ∷ textarea-placeholder "Constraints, rollout window, or audit notes"
                    ∷ textarea-required
                    ∷ textarea-dirname "notes.dir"
                    ∷ style-decls controlStyle
                    ∷ [] ❵›
          []
        ‹/› ∷
        []
      ‹/› ∷
      ‹ button ❴ button-type submitButton
                ∷ button-formmethod post
                ∷ button-formenctype urlEncoded
                ∷ style-decls buttonStyle
                ∷ [] ❵›
        text "Submit request" ∷ []
      ‹/› ∷
      []
    ‹/› ∷
    ‹ asideTag ❴ style-decls cardStyle ∷ [] ❵›
      ‹ h2 › text "Progressive controls" ∷ [] ‹/› ∷
      ‹ p ❴ style-decls mutedStyle ∷ [] ❵›
        text "The button below targets a popover and dialog-like detail panel with typed global and element-specific attributes." ∷ []
      ‹/› ∷
      ‹ button ❴ button-type plainButton
                ∷ button-popovertarget "policy-popover"
                ∷ button-popovertargetaction togglePopover
                ∷ style-decls buttonStyle
                ∷ [] ❵›
        text "Toggle policy notes" ∷ []
      ‹/› ∷
      ‹ div ❴ id "policy-popover" ∷ popover popoverManual ∷ style-decls cardStyle ∷ [] ❵›
        ‹ p › text "Popover state is exposed through the Safe global attribute set." ∷ [] ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

mediaAndEmbeds : HtmlT
mediaAndEmbeds =
  ‹ section ❴ id "media" ∷ class "two-col" ∷ style-decls sectionStyle ∷ [] ❵›
    ‹ div ❴ style-decls cardStyle ∷ [] ❵›
      ‹ h2 › text "Media" ∷ [] ‹/› ∷
      ‹ video ❴ video-src "/media/walkthrough.mp4"
                ∷ video-controls
                ∷ video-poster "/media/walkthrough-poster.jpg"
                ∷ video-playsinline
                ∷ video-loading lazy
                ∷ video-controlslist-keywords (controlsCons noDownload (controlsOne noRemotePlayback))
                ∷ [] ❵›
        []
      ‹/› ∷
      ‹ audio ❴ audio-src "/media/summary.mp3"
                ∷ audio-controls
                ∷ audio-preload preloadMetadata
                ∷ audio-controlslist-keyword noDownload
                ∷ [] ❵›
        []
      ‹/› ∷
      []
    ‹/› ∷
    ‹ div ❴ style-decls cardStyle ∷ [] ❵›
      ‹ h2 › text "Embeds and disclosure" ∷ [] ‹/› ∷
      ‹ iframe ❴ iframe-src "/embed/status"
                 ∷ iframe-loading lazy
                 ∷ iframe-sandbox-tokens (sandboxCons allowScripts (sandboxOne allowSameOrigin))
                 ∷ iframe-allow "fullscreen"
                 ∷ iframe-csp "default-src 'self'"
                 ∷ [] ❵›
        []
      ‹/› ∷
      ‹ details ❴ details-name "notes" ∷ details-open ∷ [] ❵›
        ‹ summary › text "Audit notes" ∷ [] ‹/› ∷
        ‹ p ❴ style-decls mutedStyle ∷ [] ❵›
          text "Details elements have typed open/name attributes in the Safe spec." ∷ []
        ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

webComponentTemplate : HtmlT
webComponentTemplate =
  ‹ template ❴ template-shadowrootmode shadowRootOpen
             ∷ template-shadowrootserializable
             ∷ template-shadowrootslotassignment namedSlotAssignment
             ∷ [] ❵›
    ‹ section ❴ style-decls cardStyle ∷ [] ❵›
      ‹ h2 › text "Projected detail" ∷ [] ‹/› ∷
      ‹ slot ❴ slot-name "detail" ∷ [] ❵›
        text "Fallback detail from the template." ∷ []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

dashboardPage : HtmlT
dashboardPage =
  ‹ html ❴ attribute langAttr (language "en") ∷ [] ❵›
    documentHead ∷
    ‹ body ❴ class "safe-html-showcase"
             ∷ style-decls bodyStyle
             ∷ data- "generated-by" "HTML.Generate"
             ∷ [] ❵›
      ‹ div ❴ class "shell" ∷ style-decls shellStyle ∷ [] ❵›
        topBar ∷
        hero ∷
        metrics ∷
        reportTable ∷
        intakeForm ∷
        mediaAndEmbeds ∷
        webComponentTemplate ∷
        ‹ footerTag ❴ style-decls mutedStyle ∷ [] ❵›
          text "Generated by an Agda reflection macro from typed Safe HTML." ∷ []
        ‹/› ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

componentGalleryPage : HtmlT
componentGalleryPage =
  ‹ html ❴ attribute langAttr (language "en") ∷ [] ❵›
    documentHead ∷
    ‹ body ❴ style-decls bodyStyle ∷ [] ❵›
      ‹ main ❴ style-decls shellStyle ∷ [] ❵›
        ‹ h1 › text "Component gallery" ∷ [] ‹/› ∷
        metrics ∷
        intakeForm ∷
        mediaAndEmbeds ∷
        []
      ‹/› ∷
      []
    ‹/› ∷
    []
  ‹/›

renderedDashboardPage : String
renderedDashboardPage = render renderer dashboardPage

renderedComponentGalleryPage : String
renderedComponentGalleryPage = render renderer componentGalleryPage