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

Agda.Interaction.Highlighting.LaTeX.Base

Description

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

Synopsis

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 #