ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Highlighting.LaTeX.Base

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

2 types
1 class
3 values

PackageAgda-2.8.0.2
Exports6
LanguageHaskell2010
LicenceMIT
SourceBase.hs

datadata LaTeXOptions

Constructors

LaTeXOptions
- 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.

valuegenerateLaTeXIO

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

Generates a LaTeX file for the given interface.

valueprepareCommonAssets :: (MonadLogLaTeX m, MonadIO m) => FilePath -> m ()

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

classclass Monad m => MonadLogLaTeX (m :: Type -> Type) where

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 ()

Instances1MonadLogLaTeX

MonadDebug m => MonadLogLaTeX (LogLaTeXDebugT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.LaTeX.Backend

datadata LogMessage

Constructors

LogMessage Debug Text [Text]

Instances1Show

Show LogMessageDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.LaTeX.Base

valuelogMsgToText :: LogMessage -> Text