Options for HTML generation
Constructors
Instances1Eq
Eq HtmlOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.Base
ModuleAgda-2.8.0.2Haskell2010
Agda.Interaction.Highlighting.HTML.Base
Function for generating highlighted, hyperlinked HTML from Agda sources.
Synopsis
- data HtmlOptions
- data HtmlHighlight
- value prepareCommonDestinationAssets
- value srcFileOfInterface
- value defaultPageGen
- class MonadLogHtml
- type LogHtmlT
- value runLogHtmlWith
- PackageAgda-2.8.0.2
- Exports8
- LanguageHaskell2010
- LicenceMIT
- SourceBase.hs
Determine how to highlight the file
Instances5Eq, Show, Generic, NFData, Rep
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 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.Base"HtmlHighlight"
"Agda.Interaction.Highlighting.HTML.Base"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"HighlightAll"
'PrefixI 'False) U1 :+: (C1 ('MetaCons"HighlightCode"
'PrefixI 'False) U1 :+: C1 ('MetaCons"HighlightAuto"
'PrefixI 'False) U1))
Bundle up the highlighting info for a source file
Methods
logHtml :: HtmlLogAction m
Instances1MonadLogHtml
Monad m => MonadLogHtml (LogHtmlT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.HTML.Base