Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Highlighting.LaTeX.Base

Description

Function for generating highlighted and aligned LaTeX from literate Agda source.

Synopsis

data LaTeXOptions = LaTeXOptions {
- latexOptOutDir :: FilePath
- latexOptSourceFileName :: Maybe RangeFile
- latexOptCountClusters :: Bool
}
generateLaTeXIO :: (MonadLogLaTeX m, MonadIO m) => LaTeXOptions -> Interface -> m ()
prepareCommonAssets :: (MonadLogLaTeX m, MonadIO m) => FilePath -> m ()
class Monad m => MonadLogLaTeX (m :: Type -> Type) where
- logLaTeX :: LogMessage -> m ()
data LogMessage = LogMessage Debug Text [Text]
logMsgToText :: LogMessage -> Text

Documentation

data LaTeXOptions Source #

Constructors

LaTeXOptions

Fields

latexOptOutDir :: FilePath
latexOptSourceFileName :: Maybe RangeFile
The parser uses a Position which includes a source filename for error reporting and such. We don't actually get the source filename with an Interface, and it isn't necessary to look it up. This is a "nice-to-have" parameter.
latexOptCountClusters :: Bool
Count extended grapheme clusters rather than code points when generating LaTeX.

generateLaTeXIO :: (MonadLogLaTeX m, MonadIO m) => LaTeXOptions -> Interface -> m () Source #

Generates a LaTeX file for the given interface.

prepareCommonAssets :: (MonadLogLaTeX m, MonadIO m) => FilePath -> m () Source #

Create the common base output directory and check for/install the style file.

class Monad m => MonadLogLaTeX (m :: Type -> Type) where Source #

Log LaTeX messages using a provided action.

This could be accomplished by putting logs into the RWST output and splitting it into a WriterT, but that becomes slightly more complicated to reason about in the presence of IO exceptions.

We want the logging to be reasonably polymorphic, avoid space leaks that can occur with WriterT, and also be usable during outer phases such as directory preparation.

Methods

logLaTeX :: LogMessage -> m () Source #

data LogMessage Source #

Constructors

LogMessage Debug Text [Text]

Instances

Instances details

Show LogMessage Source #
Instance details Defined in Agda.Interaction.Highlighting.LaTeX.Base Methods showsPrec :: Int -> LogMessage -> ShowS # show :: LogMessage -> String # showList :: [LogMessage] -> ShowS #

logMsgToText :: LogMessage -> Text Source #