Options for HTML generation
Constructors
Instances1Eq
Eq HtmlOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.Base
:: a typeCtrl KGHC 9.14.1 · lts/ghc-9.14.x · 45dd537 · 2026-10-11
ModuleAgda-2.8.0.2Haskell2010
Function for generating highlighted, hyperlinked HTML from Agda sources.
Options for HTML generation
Eq HtmlOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.BaseDetermine how to highlight the file
Eq HtmlHighlightDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.BaseShow HtmlHighlightDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.BaseGeneric HtmlHighlightDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.BaseNFData HtmlHighlightDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.Basetype Rep HtmlHighlight = D1 ('MetaData "HtmlHighlight"
"Agda.Interaction.Highlighting.HTML.Base"
"Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB"
'False) (C1 ('MetaCons "HighlightAll"
'PrefixI 'False) U1 :+: (C1 ('MetaCons "HighlightCode"
'PrefixI 'False) U1 :+: C1 ('MetaCons "HighlightAuto"
'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.BaseBundle up the highlighting info for a source file
logHtml :: HtmlLogAction mMonad m => MonadLogHtml (LogHtmlT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.Base