module FF.HTML.Spec.Safe.Syntax.Examples where
open import Agda.Builtin.String using (String)
open import Cubical.Data.List.Base using ([]; _∷_)
open import FF.HTML.Render using (render)
open import FF.HTML.Spec.Safe.Syntax
plainApiCard : HtmlT
plainApiCard =
el div
(class "card" ∷ id "welcome" ∷ [])
(text "Hello from the plain API" ∷ [])
anonymousCloseCard : HtmlT
anonymousCloseCard =
‹ div ❴ class "card" ∷ id "anonymous-close" ∷ [] ❵›
‹ h1 › text "Anonymous close" ∷ [] ‹/› ∷
‹ p ❴ class "lead" ∷ [] ❵›
text "The closing token closes the current node."
∷ [] ‹/› ∷
‹ a ❴ href "https://developer.mozilla.org/" ∷ rel-keyword relNoreferrer ∷ [] ❵›
text "Read MDN"
∷ [] ‹/› ∷
[]
‹/›
emptyAttributeList : HtmlT
emptyAttributeList =
‹ ul ›
‹ li › text "First" ∷ [] ‹/› ∷
‹ li › text "Second" ∷ [] ‹/› ∷
‹ li › text "Third" ∷ [] ‹/› ∷
[]
‹/›
simpleGlyphPanel : HtmlT
simpleGlyphPanel =
⟨ section ❴ class "panel" ∷ [] ❵⟩
⟨ div ❴ class "panel-heading" ∷ [] ❵⟩
text "Metrics"
∷ [] ⟨/⟩ ∷
⟨ div ❴ class "panel-body" ∷ [] ❵⟩
text "42 active proofs"
∷ [] ⟨/⟩ ∷
[]
⟨/⟩
namedWrapperCard : HtmlT
namedWrapperCard =
‹div❴ class "card named" ∷ [] ❵›
‹h1› text "Named wrappers" ∷ [] ‹/h1› ∷
‹p›
text "Specific wrappers use named closing tokens."
∷ [] ‹/p› ∷
‹a❴ href "/docs" ∷ class "button" ∷ [] ❵›
text "Open docs"
∷ [] ‹/a› ∷
[]
‹/div›
signupForm : HtmlT
signupForm =
‹ form ❴ action "/signup" ∷ method post ∷ class "signup" ∷ [] ❵›
‹ label ❴ for "email" ∷ class "label" ∷ [] ❵›
text "Email"
∷ [] ‹/› ∷
‹ input ❴ input-type emailInput
∷ input-name "email"
∷ id "email"
∷ placeholder "[email protected]"
∷ required
∷ [] ❵›
[]
‹/› ∷
‹button❴ button-type submitButton ∷ class "primary" ∷ [] ❵›
text "Join"
∷ [] ‹/button› ∷
[]
‹/›
resourceHead : HtmlT
resourceHead =
‹ head ›
‹ title-tag › text "Typed Safe HTML" ∷ [] ‹/› ∷
void Feature.voidMeta
(meta-charset "utf-8" ∷ [])
∷
void Feature.voidMeta
( meta-name "theme-color"
∷ meta-content "#1446a0"
∷ meta-media "(prefers-color-scheme: dark)"
∷ []
)
∷
void Feature.voidLink
( link-rel-keyword relPreload
∷ link-href "/assets/hero.avif"
∷ link-as asImage
∷ link-imagesrcset "/assets/hero.avif 1x, /assets/[email protected] 2x"
∷ link-imagesizes "100vw"
∷ link-fetchpriority high
∷ link-blocking blockRender
∷ []
)
∷
‹ script ❴ script-src "/assets/app.mjs"
∷ script-type moduleScript
∷ script-defer
∷ script-attributionsrc attributionPresent
∷ [] ❵›
[]
‹/› ∷
[]
‹/›
mediaFeaturePanel : HtmlT
mediaFeaturePanel =
‹ section ❴ class "media-panel" ∷ [] ❵›
void Feature.voidImg
( src "/assets/hero.png"
∷ alt "Dashboard overview"
∷ img-attributionsrc (attributionUrls (urls "https://metrics.example/register-source"))
∷ img-fetchpriority high
∷ img-loading eager
∷ []
)
∷
‹ audio ❴ audio-src "/media/intro.mp3"
∷ audio-controls
∷ audio-controlslist-keyword noDownload
∷ audio-preload preloadMetadata
∷ audio-loading lazy
∷ [] ❵›
[]
‹/› ∷
‹ video ❴ video-src "/media/demo.mp4"
∷ video-controls
∷ video-poster "/media/demo-poster.jpg"
∷ video-playsinline
∷ video-loading lazy
∷ video-controlslist-keywords (controlsCons noDownload (controlsOne noRemotePlayback))
∷ [] ❵›
[]
‹/› ∷
[]
‹/›
imageMapFeature : HtmlT
imageMapFeature =
‹ div ❴ class "image-map" ∷ [] ❵›
void Feature.voidImg
( src "/assets/product-map.png"
∷ alt "Product regions"
∷ img-usemap "#product-map"
∷ []
)
∷
‹ image-map ❴ map-name "product-map" ∷ [] ❵›
void Feature.voidArea
( area-shape rect
∷ area-coords "0,0,160,90"
∷ area-href "/product/alpha"
∷ area-alt "Alpha region"
∷ area-target self
∷ []
)
∷
void Feature.voidArea
( area-shape circle
∷ area-coords "240,120,48"
∷ area-href "/product/beta"
∷ area-alt "Beta region"
∷ area-rel-keyword relNofollow
∷ []
)
∷ []
‹/› ∷
[]
‹/›
formFeaturePanel : HtmlT
formFeaturePanel =
‹ form ❴ action "/profile"
∷ method post
∷ form-accept "image/png,image/jpeg"
∷ form-autocomplete autocompleteOn
∷ accept-charset "UTF-8"
∷ class "profile-form"
∷ [] ❵›
void Feature.voidInput
( input-type textInput
∷ input-name "displayName"
∷ input-autocomplete (autocompleteTokens "name")
∷ input-dirname "displayName.dir"
∷ []
)
∷
void Feature.voidInput
( input-type fileInput
∷ input-name "avatar"
∷ input-accept "image/png,image/jpeg"
∷ input-autocomplete autocompleteOff
∷ []
)
∷
void Feature.voidInput
( input-type colorInput
∷ input-name "accent"
∷ input-alpha
∷ input-colorspace displayP3
∷ []
)
∷
‹ select ❴ id "plan"
∷ select-size "3"
∷ select-required
∷ select-autocomplete autocompleteOff
∷ [] ❵›
‹ option › text "Starter" ∷ [] ‹/› ∷
‹ option › text "Team" ∷ [] ‹/› ∷
[]
‹/› ∷
‹ textarea ❴ textarea-placeholder "Short bio"
∷ textarea-required
∷ textarea-dirname "bio.dir"
∷ [] ❵›
[]
‹/› ∷
‹ button ❴ button-type plainButton
∷ button-command showPopoverCommand
∷ button-commandfor "profile-menu"
∷ button-popovertarget "profile-menu"
∷ button-popovertargetaction togglePopover
∷ [] ❵›
text "Open menu" ∷ []
‹/› ∷
‹ button ❴ button-type submitButton
∷ button-formenctype multipartFormData
∷ button-formmethod post
∷ button-formtarget self
∷ [] ❵›
text "Save profile" ∷ []
‹/› ∷
[]
‹/›
embeddedFeaturePanel : HtmlT
embeddedFeaturePanel =
‹ section ❴ class "embedded" ∷ [] ❵›
‹ iframe ❴ iframe-src "/embed/report"
∷ iframe-loading lazy
∷ iframe-sandbox-tokens (sandboxCons allowScripts (sandboxOne allowSameOrigin))
∷ iframe-allow "fullscreen"
∷ iframe-csp "default-src 'self'"
∷ iframe-credentialless
∷ iframe-private-token "issuer=https://issuer.example"
∷ [] ❵›
[]
‹/› ∷
‹ object ❴ object-data "/assets/chart.svg"
∷ object-usemap "#product-map"
∷ [] ❵›
text "Chart fallback" ∷ []
‹/› ∷
‹ fencedframe ❴ fencedframe-allow "shared-storage"
∷ fencedframe-width "640"
∷ fencedframe-height "360"
∷ [] ❵›
[]
‹/› ∷
[]
‹/›
interactiveFeaturePanel : HtmlT
interactiveFeaturePanel =
‹ section ❴ class "interactive" ∷ [] ❵›
‹ details ❴ details-name "safe-mdn"
∷ details-open
∷ [] ❵›
‹ summary › text "Typed disclosure" ∷ [] ‹/› ∷
‹ p › text "The name attribute groups disclosure widgets." ∷ [] ‹/› ∷
[]
‹/› ∷
‹ dialog ❴ id "confirm-dialog"
∷ dialog-closedby closedByCloseRequest
∷ popover popoverHint
∷ [] ❵›
‹ p › text "Dialog close behavior is represented by an enum." ∷ [] ‹/› ∷
[]
‹/› ∷
‹ geolocation ❴ geolocation-autolocate
∷ geolocation-watch
∷ [] ❵›
[]
‹/› ∷
[]
‹/›
shadowTemplateFeature : HtmlT
shadowTemplateFeature =
‹ template ❴ template-shadowrootmode shadowRootOpen
∷ template-shadowrootserializable
∷ template-shadowrootslotassignment namedSlotAssignment
∷ [] ❵›
‹ p ›
text "Shadow root content" ∷
‹ slot ❴ slot-name "description" ∷ [] ❵›
text "Default description" ∷ []
‹/› ∷
[]
‹/› ∷
[]
‹/›
legacyCompatibilityFeature : HtmlT
legacyCompatibilityFeature =
‹ section ❴ class "legacy-compatibility" ∷ [] ❵›
void Feature.voidHr
( legacy-align alignHr "center"
∷ legacy-color colorHr "#888888"
∷ []
)
∷
‹ table ❴ table-summary "Legacy compatibility attribute coverage"
∷ legacy-align alignTable "center"
∷ legacy-background backgroundTable "/assets/table-bg.png"
∷ legacy-bgcolor bgColorTable "#ffffff"
∷ legacy-border borderTable "1"
∷ [] ❵›
‹ caption ❴ legacy-align alignCaption "top" ∷ [] ❵›
text "Compatibility table" ∷ []
‹/› ∷
‹ tbody ❴ legacy-bgcolor bgColorTbody "#f8f8f8" ∷ [] ❵›
‹ tr ❴ legacy-align alignTr "left" ∷ [] ❵›
‹ td ❴ legacy-bgcolor bgColorTd "#eeeeee" ∷ [] ❵›
text "Legacy row" ∷ []
‹/› ∷
‹ th ❴ legacy-bgcolor bgColorTh "#dddddd" ∷ [] ❵›
text "Legacy heading" ∷ []
‹/› ∷
[]
‹/› ∷
[]
‹/› ∷
[]
‹/› ∷
[]
‹/›
safeFeatureDocument : HtmlT
safeFeatureDocument =
‹ html ›
resourceHead ∷
‹ body ❴ class "safe-demo" ∷ [] ❵›
mediaFeaturePanel ∷
imageMapFeature ∷
formFeaturePanel ∷
embeddedFeaturePanel ∷
interactiveFeaturePanel ∷
shadowTemplateFeature ∷
legacyCompatibilityFeature ∷
[]
‹/› ∷
[]
‹/›
mixedPage : HtmlT
mixedPage =
‹ main ❴ class "page" ∷ [] ❵›
‹ section ❴ class "hero" ∷ [] ❵›
‹h1› text "Typed HTML syntax" ∷ [] ‹/h1› ∷
‹ p ❴ class "lead" ∷ [] ❵›
text "Generic, glyph, and named forms can be mixed."
∷ [] ‹/› ∷
‹ a ❴ href "/start" ∷ class "button" ∷ target self ∷ [] ❵›
text "Start"
∷ [] ‹/› ∷
[]
‹/› ∷
simpleGlyphPanel ∷
signupForm ∷
[]
‹/›
renderedMixedPage : String
renderedMixedPage = render renderer mixedPage
renderedSafeFeatureDocument : String
renderedSafeFeatureDocument = render renderer safeFeatureDocument