module FF.HTML.Spec.Safe.Feature where
open import Agda.Primitive using (lzero) renaming (Set to Type)
open import FF.HTML.Spec.Safe.Tag
data MainRoot : TagName -> Type lzero where
mainRootHtml : MainRoot htmlTag
data DocumentMetadata : TagName -> Type lzero where
metadataBase : DocumentMetadata baseTag
metadataHead : DocumentMetadata headTag
metadataLink : DocumentMetadata linkTag
metadataMeta : DocumentMetadata metaTag
metadataStyle : DocumentMetadata styleTag
metadataTitle : DocumentMetadata titleTag
data SectioningRoot : TagName -> Type lzero where
sectioningRootBody : SectioningRoot bodyTag
data ContentSectioning : TagName -> Type lzero where
sectioningAddress : ContentSectioning addressTag
sectioningArticle : ContentSectioning articleTag
sectioningAside : ContentSectioning asideTag
sectioningFooter : ContentSectioning footerTag
sectioningHeader : ContentSectioning headerTag
sectioningH1 : ContentSectioning h1Tag
sectioningH2 : ContentSectioning h2Tag
sectioningH3 : ContentSectioning h3Tag
sectioningH4 : ContentSectioning h4Tag
sectioningH5 : ContentSectioning h5Tag
sectioningH6 : ContentSectioning h6Tag
sectioningHgroup : ContentSectioning hgroupTag
sectioningMain : ContentSectioning mainTag
sectioningNav : ContentSectioning navTag
sectioningSection : ContentSectioning sectionTag
sectioningSearch : ContentSectioning searchTag
data TextContent : TagName -> Type lzero where
textBlockquote : TextContent blockquoteTag
textDd : TextContent ddTag
textDiv : TextContent divTag
textDl : TextContent dlTag
textDt : TextContent dtTag
textFigcaption : TextContent figcaptionTag
textFigure : TextContent figureTag
textHr : TextContent hrTag
textLi : TextContent liTag
textMenu : TextContent menuTag
textOl : TextContent olTag
textP : TextContent pTag
textPre : TextContent preTag
textUl : TextContent ulTag
data InlineTextSemantics : TagName -> Type lzero where
inlineA : InlineTextSemantics aTag
inlineAbbr : InlineTextSemantics abbrTag
inlineB : InlineTextSemantics bTag
inlineBdi : InlineTextSemantics bdiTag
inlineBdo : InlineTextSemantics bdoTag
inlineBr : InlineTextSemantics brTag
inlineCite : InlineTextSemantics citeTag
inlineCode : InlineTextSemantics codeTag
inlineData : InlineTextSemantics dataTag
inlineDfn : InlineTextSemantics dfnTag
inlineEm : InlineTextSemantics emTag
inlineI : InlineTextSemantics iTag
inlineKbd : InlineTextSemantics kbdTag
inlineMark : InlineTextSemantics markTag
inlineQ : InlineTextSemantics qTag
inlineRp : InlineTextSemantics rpTag
inlineRt : InlineTextSemantics rtTag
inlineRuby : InlineTextSemantics rubyTag
inlineS : InlineTextSemantics sTag
inlineSamp : InlineTextSemantics sampTag
inlineSmall : InlineTextSemantics smallTag
inlineSpan : InlineTextSemantics spanTag
inlineStrong : InlineTextSemantics strongTag
inlineSub : InlineTextSemantics subTag
inlineSup : InlineTextSemantics supTag
inlineTime : InlineTextSemantics timeTag
inlineU : InlineTextSemantics uTag
inlineVar : InlineTextSemantics varTag
inlineWbr : InlineTextSemantics wbrTag
data ImageMultimedia : TagName -> Type lzero where
mediaArea : ImageMultimedia areaTag
mediaAudio : ImageMultimedia audioTag
mediaImg : ImageMultimedia imgTag
mediaMap : ImageMultimedia imageMapTag
mediaTrack : ImageMultimedia trackTag
mediaVideo : ImageMultimedia videoTag
data EmbeddedContent : TagName -> Type lzero where
embeddedEmbed : EmbeddedContent embedTag
embeddedFencedframe : EmbeddedContent fencedframeTag
embeddedIframe : EmbeddedContent iframeTag
embeddedObject : EmbeddedContent objectTag
embeddedPicture : EmbeddedContent pictureTag
embeddedSource : EmbeddedContent sourceTag
data Scripting : TagName -> Type lzero where
scriptingCanvas : Scripting canvasTag
scriptingNoscript : Scripting noscriptTag
scriptingScript : Scripting scriptTag
data DemarcatingEdits : TagName -> Type lzero where
editDel : DemarcatingEdits delTag
editIns : DemarcatingEdits insTag
data TableContent : TagName -> Type lzero where
tableCaption : TableContent captionTag
tableCol : TableContent colTag
tableColgroup : TableContent colgroupTag
tableTable : TableContent tableTag
tableTbody : TableContent tbodyTag
tableTd : TableContent tdTag
tableTfoot : TableContent tfootTag
tableTh : TableContent thTag
tableThead : TableContent theadTag
tableTr : TableContent trTag
data FormElement : TagName -> Type lzero where
formButton : FormElement buttonTag
formDatalist : FormElement datalistTag
formFieldset : FormElement fieldsetTag
formForm : FormElement formTag
formInput : FormElement inputTag
formLabel : FormElement labelTag
formLegend : FormElement legendTag
formMeter : FormElement meterTag
formOptgroup : FormElement optgroupTag
formOption : FormElement optionTag
formOutput : FormElement outputTag
formProgress : FormElement progressTag
formSelect : FormElement selectTag
formSelectedcontent : FormElement selectedcontentTag
formTextarea : FormElement textareaTag
data InteractiveElement : TagName -> Type lzero where
interactiveDetails : InteractiveElement detailsTag
interactiveDialog : InteractiveElement dialogTag
interactiveGeolocation : InteractiveElement geolocationTag
interactiveSummary : InteractiveElement summaryTag
data WebComponentElement : TagName -> Type lzero where
webComponentSlot : WebComponentElement slotTag
webComponentTemplate : WebComponentElement templateTag
data VoidElement : TagName -> Type lzero where
voidArea : VoidElement areaTag
voidBase : VoidElement baseTag
voidBr : VoidElement brTag
voidCol : VoidElement colTag
voidEmbed : VoidElement embedTag
voidHr : VoidElement hrTag
voidImg : VoidElement imgTag
voidInput : VoidElement inputTag
voidLink : VoidElement linkTag
voidMeta : VoidElement metaTag
voidSource : VoidElement sourceTag
voidTrack : VoidElement trackTag
voidWbr : VoidElement wbrTag
data RawTextElement : TagName -> Type lzero where
rawScript : RawTextElement scriptTag
rawStyle : RawTextElement styleTag
data EscapableRawTextElement : TagName -> Type lzero where
escapableTitle : EscapableRawTextElement titleTag
escapableTextarea : EscapableRawTextElement textareaTag