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

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 Source # show :: LogMessage -> String Source # showList :: [LogMessage] -> ShowS Source #

logMsgToText :: LogMessage -> Text Source #