Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Highlighting.HTML.Base

Description

Function for generating highlighted, hyperlinked HTML from Agda sources.

Synopsis

- data HtmlOptions = HtmlOptions {
  - htmlOptDir :: FilePath
  - htmlOptHighlight :: HtmlHighlight
  - htmlOptHighlightOccurrences :: Bool
  - htmlOptCssFile :: Maybe FilePath
  }
- data HtmlHighlight
  - = HighlightAll
  - | HighlightCode
  - | HighlightAuto
- prepareCommonDestinationAssets :: MonadIO m => HtmlOptions -> m ()
- srcFileOfInterface :: TopLevelModuleName -> Interface -> HtmlInputSourceFile
- defaultPageGen :: (MonadIO m, MonadLogHtml m) => HtmlOptions -> HtmlInputSourceFile -> m ()
- class MonadLogHtml (m :: Type -> Type) where
  - logHtml :: HtmlLogAction m
- type LogHtmlT (m :: Type -> Type) = ReaderT (HtmlLogAction m) m
- runLogHtmlWith :: Monad m => HtmlLogAction m -> LogHtmlT m a -> m a

# Documentation

data HtmlOptions Source #

Options for HTML generation

Constructors

HtmlOptions |

Fields

- htmlOptDir :: FilePath
- htmlOptHighlight :: HtmlHighlight
- htmlOptHighlightOccurrences :: Bool
- htmlOptCssFile :: Maybe FilePath

#### Instances

Instances details

Eq HtmlOptions Source # |
Instance details Defined in Agda.Interaction.Highlighting.HTML.Base Methods (==) :: HtmlOptions -> HtmlOptions -> Bool Source # (/=) :: HtmlOptions -> HtmlOptions -> Bool Source #

data HtmlHighlight Source #

Determine how to highlight the file

Constructors

HighlightAll |
HighlightCode |
HighlightAuto |

#### Instances

Instances details

NFData HtmlHighlight Source # |
Instance details Defined in Agda.Interaction.Highlighting.HTML.Base Methods rnf :: HtmlHighlight -> () Source #
Generic HtmlHighlight Source # |

Instance details

Defined in Agda.Interaction.Highlighting.HTML.Base

Associated Types

type Rep HtmlHighlight |

Instance details

Defined in Agda.Interaction.Highlighting.HTML.Base

type Rep HtmlHighlight = D1 ('MetaData "HtmlHighlight" "Agda.Interaction.Highlighting.HTML.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "HighlightAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "HighlightCode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HighlightAuto" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: HtmlHighlight -> Rep HtmlHighlight x Source #

to :: Rep HtmlHighlight x -> HtmlHighlight Source #

Show HtmlHighlight Source # |
Instance details Defined in Agda.Interaction.Highlighting.HTML.Base Methods showsPrec :: Int -> HtmlHighlight -> ShowS Source # show :: HtmlHighlight -> String Source # showList :: [HtmlHighlight] -> ShowS Source #
Eq HtmlHighlight Source # |
Instance details Defined in Agda.Interaction.Highlighting.HTML.Base Methods (==) :: HtmlHighlight -> HtmlHighlight -> Bool Source # (/=) :: HtmlHighlight -> HtmlHighlight -> Bool Source #
type Rep HtmlHighlight Source # |

Instance details

Defined in Agda.Interaction.Highlighting.HTML.Base

type Rep HtmlHighlight = D1 ('MetaData "HtmlHighlight" "Agda.Interaction.Highlighting.HTML.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "HighlightAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "HighlightCode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HighlightAuto" 'PrefixI 'False) (U1 :: Type -> Type)))

prepareCommonDestinationAssets :: MonadIO m => HtmlOptions -> m () Source #

srcFileOfInterface :: TopLevelModuleName -> Interface -> HtmlInputSourceFile Source #

Bundle up the highlighting info for a source file

defaultPageGen :: (MonadIO m, MonadLogHtml m) => HtmlOptions -> HtmlInputSourceFile -> m () Source #

class MonadLogHtml (m :: Type -> Type) where Source #

Methods

logHtml :: HtmlLogAction m Source #

#### Instances

Instances details

Monad m => MonadLogHtml (LogHtmlT m) Source # |
Instance details Defined in Agda.Interaction.Highlighting.HTML.Base Methods logHtml :: HtmlLogAction (LogHtmlT m) Source #

type LogHtmlT (m :: Type -> Type) = ReaderT (HtmlLogAction m) m Source #

runLogHtmlWith :: Monad m => HtmlLogAction m -> LogHtmlT m a -> m a Source #