    {-# LANGUAGE CPP #-}
    {-# LANGUAGE ViewPatterns #-}

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

    module Agda.Interaction.Highlighting.LaTeX.Base
      ( generateLaTeXIO
      , prepareCommonAssets
      , runLogLaTeXTWith
      , logMsgToText
      , LogMessage(..)
      , MonadLogLaTeX
      , LogLaTeXT
      , LaTeXOptions(..)
      ) where

    import Prelude hiding (log)

    import Data.Bifunctor (second)
    import Data.Char
    import Data.Maybe
    import Data.Function
    import Data.Foldable (toList)
    #if !(MIN_VERSION_base(4,11,0))
    import Data.Semigroup (Semigroup(..))
    #endif

    import Control.Monad (forM_, mapM_, unless, when)
    import Control.Monad.Trans.Reader as R ( ReaderT(runReaderT))
    import Control.Monad.RWS.Strict
      ( RWST(runRWST)
      , MonadReader(..), asks
      , MonadState(..), gets, modify
      , lift, tell
      )
    import Control.Monad.IO.Class
      ( MonadIO(..)
      )

    import System.Directory
    import System.Exit
    import System.FilePath
    import System.Process

    import Data.Text (Text)
    import qualified Data.Text               as T
    #ifdef COUNT_CLUSTERS
    import qualified Data.Text.ICU           as ICU
    #endif
    import qualified Data.Text.Lazy          as L
    import qualified Data.Text.Lazy.Encoding as E
    import qualified Data.ByteString.Lazy    as BS

    import Data.HashSet (HashSet)
    import qualified Data.HashSet as Set
    import qualified Data.IntMap  as IntMap
    import qualified Data.List    as List

    import Paths_Agda

    import Agda.Syntax.Abstract (toTopLevelModuleName)
    import Agda.Syntax.Common
    import Agda.Syntax.Concrete (TopLevelModuleName, moduleNameParts)
    import Agda.Syntax.Parser.Literate (literateTeX, LayerRole, atomizeLayers)
    import qualified Agda.Syntax.Parser.Literate as L
    import Agda.Syntax.Position (startPos)

    import Agda.Interaction.Highlighting.Precise hiding (toList)

    import Agda.TypeChecking.Monad (Interface(..))

    import Agda.Utils.FileName (AbsolutePath)
    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Functor  ((<&>))
    import Agda.Utils.List     (last1, updateHead, updateLast)
    import Agda.Utils.Maybe    (whenJust)
    import qualified Agda.Utils.List1 as List1

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- * Logging

    class Monad m => MonadLogLaTeX m where
      logLaTeX :: LogMessage -> m ()

    -- | 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.
    --
    -- I'm not certain this is the best way to do it, but whatever.
    type LogLaTeXT m = ReaderT (LogMessage -> m ()) m

    instance Monad m => MonadLogLaTeX (LogLaTeXT m) where
      logLaTeX :: LogMessage -> LogLaTeXT m ()
    logLaTeX LogMessage
    message = do
        LogMessage -> m ()
    doLog <- ReaderT (LogMessage -> m ()) m (LogMessage -> m ())
    forall r (m :: * -> *). MonadReader r m => m r
    ask
        m () -> LogLaTeXT m ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> LogLaTeXT m ()) -> m () -> LogLaTeXT m ()
    forall a b. (a -> b) -> a -> b
    $ LogMessage -> m ()
    doLog LogMessage
    message

    runLogLaTeXTWith :: Monad m => (LogMessage -> m ()) -> LogLaTeXT m a -> m a
    runLogLaTeXTWith :: forall (m :: * -> *) a.
    Monad m =>
    (LogMessage -> m ()) -> LogLaTeXT m a -> m a
    runLogLaTeXTWith = (ReaderT (LogMessage -> m ()) m a -> (LogMessage -> m ()) -> m a)
    -> (LogMessage -> m ()) -> ReaderT (LogMessage -> m ()) m a -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ReaderT (LogMessage -> m ()) m a -> (LogMessage -> m ()) -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT

    -- Not currently used, but for example:
    -- runLogLaTeXWithIO :: MonadIO m => LogLaTeXT m a -> m a
    -- runLogLaTeXWithIO = runLogLaTeXTWith $ liftIO . T.putStrLn . logMsgToText

    ------------------------------------------------------------------------
    -- * Datatypes.

    -- | The @LaTeX@ monad is a combination of @ExceptT@, @RWST@ and
    -- a logger @m@. The error part is just used to keep track whether we finished or
    -- not, the reader part contains static options used, the writer is where the
    -- output goes and the state is for keeping track of the tokens and some
    -- other useful info, and the MonadLogLaTeX part is used for printing debugging info.

    type LaTeX a = forall m. MonadLogLaTeX m => RWST Env [Output] State m a

    -- | Output items.

    data LogMessage = LogMessage Debug Text [Text] deriving Int -> LogMessage -> ShowS
    [LogMessage] -> ShowS
    LogMessage -> [Char]
    (Int -> LogMessage -> ShowS)
    -> (LogMessage -> [Char])
    -> ([LogMessage] -> ShowS)
    -> Show LogMessage
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [LogMessage] -> ShowS
    $cshowList :: [LogMessage] -> ShowS
    show :: LogMessage -> [Char]
    $cshow :: LogMessage -> [Char]
    showsPrec :: Int -> LogMessage -> ShowS
    $cshowsPrec :: Int -> LogMessage -> ShowS
    Show

    data Output
      = Text !Text
        -- ^ A piece of text.
      | MaybeColumn !AlignmentColumn
        -- ^ A column. If it turns out to be an indentation column that is
        --   not used to indent or align something, then no column will be
        --   generated, only whitespace ('agdaSpace').
      deriving Int -> Output -> ShowS
    [Output] -> ShowS
    Output -> [Char]
    (Int -> Output -> ShowS)
    -> (Output -> [Char]) -> ([Output] -> ShowS) -> Show Output
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [Output] -> ShowS
    $cshowList :: [Output] -> ShowS
    show :: Output -> [Char]
    $cshow :: Output -> [Char]
    showsPrec :: Int -> Output -> ShowS
    $cshowsPrec :: Int -> Output -> ShowS
    Show

    -- | Column kinds.

    data Kind
      = Indentation
        -- ^ Used only for indentation (the placement of the first token
        -- on a line, relative to tokens on previous lines).
      | Alignment
        -- ^ Used both for indentation and for alignment.
      deriving (Kind -> Kind -> Bool
    (Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Kind -> Kind -> Bool
    $c/= :: Kind -> Kind -> Bool
    == :: Kind -> Kind -> Bool
    $c== :: Kind -> Kind -> Bool
    Eq, Int -> Kind -> ShowS
    [Kind] -> ShowS
    Kind -> [Char]
    (Int -> Kind -> ShowS)
    -> (Kind -> [Char]) -> ([Kind] -> ShowS) -> Show Kind
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [Kind] -> ShowS
    $cshowList :: [Kind] -> ShowS
    show :: Kind -> [Char]
    $cshow :: Kind -> [Char]
    showsPrec :: Int -> Kind -> ShowS
    $cshowsPrec :: Int -> Kind -> ShowS
    Show)

    -- | Unique identifiers for indentation columns.

    type IndentationColumnId = Int

    -- | Alignment and indentation columns.

    data AlignmentColumn = AlignmentColumn
      { AlignmentColumn -> Int
    columnCodeBlock :: !Int
        -- ^ The column's code block.
      , AlignmentColumn -> Int
    columnColumn :: !Int
        -- ^ The column number.
      , AlignmentColumn -> Maybe Int
    columnKind :: Maybe IndentationColumnId
        -- ^ The column kind. 'Nothing' for alignment columns and @'Just'
        -- i@ for indentation columns, where @i@ is the column's unique
        -- identifier.
      } deriving Int -> AlignmentColumn -> ShowS
    [AlignmentColumn] -> ShowS
    AlignmentColumn -> [Char]
    (Int -> AlignmentColumn -> ShowS)
    -> (AlignmentColumn -> [Char])
    -> ([AlignmentColumn] -> ShowS)
    -> Show AlignmentColumn
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [AlignmentColumn] -> ShowS
    $cshowList :: [AlignmentColumn] -> ShowS
    show :: AlignmentColumn -> [Char]
    $cshow :: AlignmentColumn -> [Char]
    showsPrec :: Int -> AlignmentColumn -> ShowS
    $cshowsPrec :: Int -> AlignmentColumn -> ShowS
    Show

    -- | Type of function for estimating column width of text.

    type TextWidthEstimator = Text -> Int

    data Env = Env
      { Env -> TextWidthEstimator
    estimateTextWidth :: !TextWidthEstimator
        -- ^ How to estimate the column width of text (i.e. Count extended grapheme clusters vs. code points).
      , Env -> [Debug]
    debugs :: [Debug]
        -- ^ Says what debug information should printed.
      }

    data State = State
      { State -> Int
    codeBlock     :: !Int   -- ^ The number of the current code block.
      , State -> Int
    column        :: !Int   -- ^ The current column number.
      , State -> [AlignmentColumn]
    columns       :: [AlignmentColumn]
                                -- ^ All alignment columns found on the
                                --   current line (so far), in reverse
                                --   order.
      , State -> [AlignmentColumn]
    columnsPrev   :: [AlignmentColumn]
                                -- ^ All alignment columns found in
                                --   previous lines (in any code block),
                                --   with larger columns coming first.
      , State -> Int
    nextId        :: !IndentationColumnId
                                -- ^ The next indentation column
                                -- identifier.
      , State -> HashSet Int
    usedColumns   :: HashSet IndentationColumnId
                                -- ^ Indentation columns that have
                                -- actually
                                --   been used.
      }

    type Tokens = [Token]

    data Token = Token
      { Token -> Text
    text     :: !Text
      , Token -> Aspects
    info     :: Aspects
      }
      deriving Int -> Token -> ShowS
    [Token] -> ShowS
    Token -> [Char]
    (Int -> Token -> ShowS)
    -> (Token -> [Char]) -> ([Token] -> ShowS) -> Show Token
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [Token] -> ShowS
    $cshowList :: [Token] -> ShowS
    show :: Token -> [Char]
    $cshow :: Token -> [Char]
    showsPrec :: Int -> Token -> ShowS
    $cshowsPrec :: Int -> Token -> ShowS
    Show

    withTokenText :: (Text -> Text) -> Token -> Token
    withTokenText :: (Text -> Text) -> Token -> Token
    withTokenText Text -> Text
    f tok :: Token
    tok@Token{text :: Token -> Text
    text = Text
    t} = Token
    tok{text :: Text
    text = Text -> Text
    f Text
    t}

    data Debug = MoveColumn | NonCode | Code | Spaces | Output | FileSystem
      deriving (Debug -> Debug -> Bool
    (Debug -> Debug -> Bool) -> (Debug -> Debug -> Bool) -> Eq Debug
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Debug -> Debug -> Bool
    $c/= :: Debug -> Debug -> Bool
    == :: Debug -> Debug -> Bool
    $c== :: Debug -> Debug -> Bool
    Eq, Int -> Debug -> ShowS
    [Debug] -> ShowS
    Debug -> [Char]
    (Int -> Debug -> ShowS)
    -> (Debug -> [Char]) -> ([Debug] -> ShowS) -> Show Debug
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [Debug] -> ShowS
    $cshowList :: [Debug] -> ShowS
    show :: Debug -> [Char]
    $cshow :: Debug -> [Char]
    showsPrec :: Int -> Debug -> ShowS
    $cshowsPrec :: Int -> Debug -> ShowS
    Show)

    -- | Run function for the @LaTeX@ monad.
    runLaTeX :: MonadLogLaTeX m =>
      LaTeX a -> Env -> State -> m (a, State, [Output])
    -- ASR (2021-02-07). The eta-expansion is required by GHC >= 9.0.1
    -- (see Issue #4955).
    runLaTeX :: forall (m :: * -> *) a.
    MonadLogLaTeX m =>
    LaTeX a -> Env -> State -> m (a, State, [Output])
    runLaTeX LaTeX a
    l = RWST Env [Output] State m a
    -> Env -> State -> m (a, State, [Output])
    forall r w s (m :: * -> *) a.
    RWST r w s m a -> r -> s -> m (a, s, w)
    runRWST RWST Env [Output] State m a
    LaTeX a
    l

    emptyState :: State
    emptyState :: State
    emptyState = State :: Int
    -> Int
    -> [AlignmentColumn]
    -> [AlignmentColumn]
    -> Int
    -> HashSet Int
    -> State
    State
      { codeBlock :: Int
    codeBlock     = Int
    0
      , column :: Int
    column        = Int
    0
      , columns :: [AlignmentColumn]
    columns       = []
      , columnsPrev :: [AlignmentColumn]
    columnsPrev   = []
      , nextId :: Int
    nextId        = Int
    0
      , usedColumns :: HashSet Int
    usedColumns   = HashSet Int
    forall a. HashSet a
    Set.empty
      }

    emptyEnv
      :: TextWidthEstimator  -- ^ Count extended grapheme clusters?
      -> Env
    emptyEnv :: TextWidthEstimator -> Env
    emptyEnv TextWidthEstimator
    twe = TextWidthEstimator -> [Debug] -> Env
    Env TextWidthEstimator
    twe []

    ------------------------------------------------------------------------
    -- * Some helpers.

    -- | Gives the size of the string. If cluster counting is enabled,
    -- then the number of extended grapheme clusters is computed (the root
    -- locale is used), and otherwise the number of code points.

    size :: Text -> LaTeX Int
    size :: Text -> LaTeX Int
    size Text
    t = (Env -> TextWidthEstimator)
    -> RWST Env [Output] State m TextWidthEstimator
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks Env -> TextWidthEstimator
    estimateTextWidth RWST Env [Output] State m TextWidthEstimator
    -> (TextWidthEstimator -> Int) -> RWST Env [Output] State m Int
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> (TextWidthEstimator -> TextWidthEstimator
    forall a b. (a -> b) -> a -> b
    $ Text
    t)

    -- | Does the string consist solely of whitespace?

    isSpaces :: Text -> Bool
    isSpaces :: Text -> Bool
    isSpaces = (Char -> Bool) -> Text -> Bool
    T.all Char -> Bool
    isSpace

    -- | Is the character a whitespace character distinct from '\n'?

    isSpaceNotNewline :: Char -> Bool
    isSpaceNotNewline :: Char -> Bool
    isSpaceNotNewline Char
    c = Char -> Bool
    isSpace Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '\n'

    -- | Replaces all forms of whitespace, except for new-line characters,
    -- with spaces.

    replaceSpaces :: Text -> Text
    replaceSpaces :: Text -> Text
    replaceSpaces = (Char -> Char) -> Text -> Text
    T.map (\Char
    c -> if Char -> Bool
    isSpaceNotNewline Char
    c then Char
    ' ' else Char
    c)

    -- | If the `Token` consists of spaces, the internal column counter is advanced
    --   by the length of the token. Otherwise, `moveColumnForToken` is a no-op.
    moveColumnForToken :: Token -> LaTeX ()
    moveColumnForToken :: Token -> LaTeX ()
    moveColumnForToken Token{ text :: Token -> Text
    text = Text
    t } = do
      Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Text -> Bool
    isSpaces Text
    t) (RWST Env [Output] State m () -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ do
        Debug -> Text -> LaTeX ()
    log Debug
    MoveColumn Text
    t
        -- ASR (2021-02-07). The eta-expansion is required by GHC >= 9.0.1
        -- (see Issue #4955).
        Int
    n <- Text -> LaTeX Int
    size Text
    t
        Int -> LaTeX ()
    moveColumn Int
    n

    -- | Merges 'columns' into 'columnsPrev', resets 'column' and
    -- 'columns'

    resetColumn :: LaTeX ()
    resetColumn :: LaTeX ()
    resetColumn = (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s ->
      State
    s { column :: Int
    column      = Int
    0
        , columnsPrev :: [AlignmentColumn]
    columnsPrev = [AlignmentColumn] -> [AlignmentColumn] -> [AlignmentColumn]
    mergeCols (State -> [AlignmentColumn]
    columns State
    s) (State -> [AlignmentColumn]
    columnsPrev State
    s)
        , columns :: [AlignmentColumn]
    columns     = []
        }
      where
      -- Remove shadowed columns from old.
      mergeCols :: [AlignmentColumn] -> [AlignmentColumn] -> [AlignmentColumn]
    mergeCols []         [AlignmentColumn]
    old = [AlignmentColumn]
    old
      mergeCols new :: [AlignmentColumn]
    new@(AlignmentColumn
    n:[AlignmentColumn]
    ns) [AlignmentColumn]
    old = [AlignmentColumn]
    new [AlignmentColumn] -> [AlignmentColumn] -> [AlignmentColumn]
    forall a. [a] -> [a] -> [a]
    ++ (AlignmentColumn -> Bool) -> [AlignmentColumn] -> [AlignmentColumn]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    leastNew) (Int -> Bool)
    -> (AlignmentColumn -> Int) -> AlignmentColumn -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AlignmentColumn -> Int
    columnColumn) [AlignmentColumn]
    old
        where
        leastNew :: Int
    leastNew = AlignmentColumn -> Int
    columnColumn (AlignmentColumn -> [AlignmentColumn] -> AlignmentColumn
    forall a. a -> [a] -> a
    last1 AlignmentColumn
    n [AlignmentColumn]
    ns)

    moveColumn :: Int -> LaTeX ()
    moveColumn :: Int -> LaTeX ()
    moveColumn Int
    i = (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s -> State
    s { column :: Int
    column = Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + State -> Int
    column State
    s }

    -- | Registers a column of the given kind. The column is returned.

    registerColumn :: Kind -> LaTeX AlignmentColumn
    registerColumn :: Kind -> LaTeX AlignmentColumn
    registerColumn Kind
    kind = do
      Int
    column    <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column
      Int
    codeBlock <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    codeBlock
      Maybe Int
    colKind   <- case Kind
    kind of
                     Kind
    Alignment   -> Maybe Int -> RWST Env [Output] State m (Maybe Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Int
    forall a. Maybe a
    Nothing
                     Kind
    Indentation -> do
                       Int
    nextId <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    nextId
                       (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s -> State
    s { nextId :: Int
    nextId = Int -> Int
    forall a. Enum a => a -> a
    succ Int
    nextId }
                       Maybe Int -> RWST Env [Output] State m (Maybe Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    nextId)
      let c :: AlignmentColumn
    c = AlignmentColumn :: Int -> Int -> Maybe Int -> AlignmentColumn
    AlignmentColumn { columnColumn :: Int
    columnColumn    = Int
    column
                              , columnCodeBlock :: Int
    columnCodeBlock = Int
    codeBlock
                              , columnKind :: Maybe Int
    columnKind      = Maybe Int
    colKind
                              }
      (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s -> State
    s { columns :: [AlignmentColumn]
    columns = AlignmentColumn
    c AlignmentColumn -> [AlignmentColumn] -> [AlignmentColumn]
    forall a. a -> [a] -> [a]
    : State -> [AlignmentColumn]
    columns State
    s }
      AlignmentColumn -> RWST Env [Output] State m AlignmentColumn
    forall (m :: * -> *) a. Monad m => a -> m a
    return AlignmentColumn
    c

    -- | Registers the given column as used (if it is an indentation
    -- column).

    useColumn :: AlignmentColumn -> LaTeX ()
    useColumn :: AlignmentColumn -> LaTeX ()
    useColumn AlignmentColumn
    c = Maybe Int
    -> (Int -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (AlignmentColumn -> Maybe Int
    columnKind AlignmentColumn
    c) ((Int -> RWST Env [Output] State m ())
     -> RWST Env [Output] State m ())
    -> (Int -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i ->
      (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \ State
    s -> State
    s { usedColumns :: HashSet Int
    usedColumns = Int -> HashSet Int -> HashSet Int
    forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
    Set.insert Int
    i (State -> HashSet Int
    usedColumns State
    s) }

    -- | Alignment column zero in the current code block.

    columnZero :: LaTeX AlignmentColumn
    columnZero :: LaTeX AlignmentColumn
    columnZero = do
      Int
    codeBlock <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    codeBlock
      AlignmentColumn -> RWST Env [Output] State m AlignmentColumn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AlignmentColumn -> RWST Env [Output] State m AlignmentColumn)
    -> AlignmentColumn -> RWST Env [Output] State m AlignmentColumn
    forall a b. (a -> b) -> a -> b
    $ AlignmentColumn :: Int -> Int -> Maybe Int -> AlignmentColumn
    AlignmentColumn { columnColumn :: Int
    columnColumn    = Int
    0
                               , columnCodeBlock :: Int
    columnCodeBlock = Int
    codeBlock
                               , columnKind :: Maybe Int
    columnKind      = Maybe Int
    forall a. Maybe a
    Nothing
                               }

    -- | Registers column zero as an alignment column.

    registerColumnZero :: LaTeX ()
    registerColumnZero :: LaTeX ()
    registerColumnZero = do
      AlignmentColumn
    c <- RWST Env [Output] State m AlignmentColumn
    LaTeX AlignmentColumn
    columnZero
      (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s -> State
    s { columns :: [AlignmentColumn]
    columns = [AlignmentColumn
    c] }

    -- | Changes to the state that are performed at the start of a code
    -- block.

    enterCode :: LaTeX ()
    enterCode :: LaTeX ()
    enterCode = do
      RWST Env [Output] State m ()
    LaTeX ()
    resetColumn
      (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> RWST Env [Output] State m ())
    -> (State -> State) -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s -> State
    s { codeBlock :: Int
    codeBlock = State -> Int
    codeBlock State
    s Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 }

    -- | Changes to the state that are performed at the end of a code
    -- block.

    leaveCode :: LaTeX ()
    leaveCode :: LaTeX ()
    leaveCode = () -> RWST Env [Output] State m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    tshow :: Show a => a -> Text
    tshow :: forall a. Show a => a -> Text
    tshow = [Char] -> Text
    T.pack ([Char] -> Text) -> (a -> [Char]) -> a -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> [Char]
    forall a. Show a => a -> [Char]
    show

    logMsgToText :: LogMessage -> Text
    logMsgToText :: LogMessage -> Text
    logMsgToText (LogMessage Debug
    messageLabel Text
    text [Text]
    extra) = [Text] -> Text
    T.concat ([Text] -> Text) -> [Text] -> Text
    forall a b. (a -> b) -> a -> b
    $
      [ Debug -> Text
    forall a. Show a => a -> Text
    tshow Debug
    messageLabel, Text
    ": '", Text
    text, Text
    "' "
      ] [Text] -> [Text] -> [Text]
    forall a. [a] -> [a] -> [a]
    ++ if [Text] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Text]
    extra then [] else [Text
    "(", [Text] -> Text
    T.unwords [Text]
    extra, Text
    ")"]

    logHelper :: Debug -> Text -> [Text] -> LaTeX ()
    logHelper :: Debug -> Text -> [Text] -> LaTeX ()
    logHelper Debug
    debug Text
    text [Text]
    extra = do
      [Debug]
    logLevels <- Env -> [Debug]
    debugs (Env -> [Debug])
    -> RWST Env [Output] State m Env
    -> RWST Env [Output] State m [Debug]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RWST Env [Output] State m Env
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Debug
    debug Debug -> [Debug] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Debug]
    logLevels) (RWST Env [Output] State m () -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ do
        m () -> RWST Env [Output] State m ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> RWST Env [Output] State m ())
    -> m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ LogMessage -> m ()
    forall (m :: * -> *). MonadLogLaTeX m => LogMessage -> m ()
    logLaTeX (Debug -> Text -> [Text] -> LogMessage
    LogMessage Debug
    debug Text
    text [Text]
    extra)

    log :: Debug -> Text -> LaTeX ()
    log :: Debug -> Text -> LaTeX ()
    log Debug
    MoveColumn Text
    text = do
      [AlignmentColumn]
    cols <- (State -> [AlignmentColumn])
    -> RWST Env [Output] State m [AlignmentColumn]
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> [AlignmentColumn]
    columns
      Debug -> Text -> [Text] -> LaTeX ()
    logHelper Debug
    MoveColumn Text
    text [Text
    "columns=", [AlignmentColumn] -> Text
    forall a. Show a => a -> Text
    tshow [AlignmentColumn]
    cols]
    log Debug
    Code Text
    text = do
      [AlignmentColumn]
    cols <- (State -> [AlignmentColumn])
    -> RWST Env [Output] State m [AlignmentColumn]
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> [AlignmentColumn]
    columns
      Int
    col <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column
      Debug -> Text -> [Text] -> LaTeX ()
    logHelper Debug
    Code Text
    text [Text
    "columns=", [AlignmentColumn] -> Text
    forall a. Show a => a -> Text
    tshow [AlignmentColumn]
    cols, Text
    "col=", Int -> Text
    forall a. Show a => a -> Text
    tshow Int
    col]
    log Debug
    debug Text
    text = Debug -> Text -> [Text] -> LaTeX ()
    logHelper Debug
    debug Text
    text []

    output :: Output -> LaTeX ()
    output :: Output -> LaTeX ()
    output Output
    item = do
      Debug -> Text -> LaTeX ()
    log Debug
    Output (Text -> RWST Env [Output] State m ())
    -> Text -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Output -> Text
    forall a. Show a => a -> Text
    tshow Output
    item
      [Output] -> RWST Env [Output] State m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Output
    item]

    ------------------------------------------------------------------------
    -- * LaTeX and polytable strings.

    -- Polytable, http://www.ctan.org/pkg/polytable, is used for code
    -- alignment, similar to lhs2TeX's approach.

    nl :: Text
    nl :: Text
    nl = Text
    "%\n"

    -- | A command that is used when two tokens are put next to each other
    -- in the same column.

    agdaSpace :: Text
    agdaSpace :: Text
    agdaSpace = Text
    cmdPrefix Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "Space" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text -> Text
    cmdArg Text
    T.empty Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    nl

    -- | The column's name.
    --
    -- Indentation columns have unique names, distinct from all alignment
    -- column names.

    columnName :: AlignmentColumn -> Text
    columnName :: AlignmentColumn -> Text
    columnName AlignmentColumn
    c = [Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ case AlignmentColumn -> Maybe Int
    columnKind AlignmentColumn
    c of
      Maybe Int
    Nothing -> Int -> [Char]
    forall a. Show a => a -> [Char]
    show (AlignmentColumn -> Int
    columnColumn AlignmentColumn
    c)
      Just Int
    i  -> Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "I"

    -- | Opens a column with the given name.

    ptOpen' :: Text -> Text
    ptOpen' :: Text -> Text
    ptOpen' Text
    name = Text
    "\\>[" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    name Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "]"

    -- | Opens the given column.

    ptOpen :: AlignmentColumn -> Text
    ptOpen :: AlignmentColumn -> Text
    ptOpen AlignmentColumn
    c = Text -> Text
    ptOpen' (AlignmentColumn -> Text
    columnName AlignmentColumn
    c)

    -- | Opens a special column that is only used at the beginning of
    -- lines.

    ptOpenBeginningOfLine :: Text
    ptOpenBeginningOfLine :: Text
    ptOpenBeginningOfLine = Text -> Text
    ptOpen' Text
    "." Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "[@{}l@{}]"

    -- | Opens the given column, and inserts an indentation instruction
    -- with the given argument at the end of it.

    ptOpenIndent
      :: AlignmentColumn
      -> Int              -- ^ Indentation instruction argument.
      -> Text
    ptOpenIndent :: AlignmentColumn -> Int -> Text
    ptOpenIndent AlignmentColumn
    c Int
    delta =
      AlignmentColumn -> Text
    ptOpen AlignmentColumn
    c Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "[@{}l@{"
               Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    cmdPrefix
               Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "Indent"
               Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text -> Text
    cmdArg ([Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    delta)
               Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "}]"

    ptClose :: Text
    ptClose :: Text
    ptClose = Text
    "\\<"

    ptClose' :: AlignmentColumn -> Text
    ptClose' :: AlignmentColumn -> Text
    ptClose' AlignmentColumn
    c =
      Text
    ptClose Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "[" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> AlignmentColumn -> Text
    columnName AlignmentColumn
    c Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "]"

    ptNL :: Text
    ptNL :: Text
    ptNL = Text
    nl Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "\\\\\n"

    ptEmptyLine :: Text
    ptEmptyLine :: Text
    ptEmptyLine =
      Text
    nl Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "\\\\["
         Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    cmdPrefix
         Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "EmptyExtraSkip"
         Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "]%\n"

    cmdPrefix :: Text
    cmdPrefix :: Text
    cmdPrefix = Text
    "\\Agda"

    cmdArg :: Text -> Text
    cmdArg :: Text -> Text
    cmdArg Text
    x = Text
    "{" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    x Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "}"

    ------------------------------------------------------------------------
    -- * Output generation from a stream of labelled tokens.

    processLayers :: [(LayerRole, Tokens)] -> LaTeX ()
    -- ASR (2021-02-07). The eta-expansion on @lt@ is required by GHC >=
    -- 9.0.1 (see Issue #4955).
    processLayers :: [(LayerRole, [Token])] -> LaTeX ()
    processLayers [(LayerRole, [Token])]
    lt = [(LayerRole, [Token])]
    -> ((LayerRole, [Token]) -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(LayerRole, [Token])]
    lt (((LayerRole, [Token]) -> RWST Env [Output] State m ())
     -> RWST Env [Output] State m ())
    -> ((LayerRole, [Token]) -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \ (LayerRole
    layerRole,[Token]
    toks) -> do
      case LayerRole
    layerRole of
        LayerRole
    L.Markup  -> [Token] -> LaTeX ()
    processMarkup  [Token]
    toks
        LayerRole
    L.Comment -> [Token] -> LaTeX ()
    processComment [Token]
    toks
        LayerRole
    L.Code    -> [Token] -> LaTeX ()
    processCode    [Token]
    toks

    -- | Deals with markup, which is output verbatim.
    processMarkup :: Tokens -> LaTeX ()
    -- ASR (2021-02-07). The eta-expansion on @ts@ is required by GHC >=
    -- 9.0.1 (see Issue #4955).
    processMarkup :: [Token] -> LaTeX ()
    processMarkup [Token]
    ts = [Token]
    -> (Token -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Token]
    ts ((Token -> RWST Env [Output] State m ())
     -> RWST Env [Output] State m ())
    -> (Token -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \ Token
    t' -> do
      Token -> LaTeX ()
    moveColumnForToken Token
    t'
      Output -> LaTeX ()
    output (Text -> Output
    Text (Token -> Text
    text Token
    t'))

    -- | Deals with literate text, which is output verbatim
    processComment :: Tokens -> LaTeX ()
    -- ASR (2021-02-07). The eta-expansion with @ts@ is required by GHC >=
    -- 9.0.1 (see Issue #4955).
    processComment :: [Token] -> LaTeX ()
    processComment [Token]
    ts = [Token]
    -> (Token -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Token]
    ts ((Token -> RWST Env [Output] State m ())
     -> RWST Env [Output] State m ())
    -> (Token -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ \ Token
    t' -> do
      Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Text
    "%" Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Text -> Text
    T.take Int
    1 (Text -> Text
    T.stripStart (Token -> Text
    text Token
    t'))) (RWST Env [Output] State m () -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ do
        Token -> LaTeX ()
    moveColumnForToken Token
    t'
      Output -> LaTeX ()
    output (Text -> Output
    Text (Token -> Text
    text Token
    t'))

    -- | Deals with code blocks. Every token, except spaces, is pretty
    -- printed as a LaTeX command.
    processCode :: Tokens -> LaTeX ()
    processCode :: [Token] -> LaTeX ()
    processCode [Token]
    toks' = do
      Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text Text
    nl
      RWST Env [Output] State m ()
    LaTeX ()
    enterCode
      (Token -> RWST Env [Output] State m ())
    -> [Token] -> RWST Env [Output] State m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Token -> RWST Env [Output] State m ()
    forall {m :: * -> *}.
    MonadLogLaTeX m =>
    Token -> RWST Env [Output] State m ()
    go [Token]
    toks'
      Int -> RWST Env [Output] State m ()
    forall {m :: * -> *} {a}.
    (Eq a, Num a, MonadLogLaTeX m) =>
    a -> RWST Env [Output] State m ()
    ptOpenWhenColumnZero (Int -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m Int -> RWST Env [Output] State m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column
      Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text (Text -> Output) -> Text -> Output
    forall a b. (a -> b) -> a -> b
    $ Text
    ptClose Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    nl
      RWST Env [Output] State m ()
    LaTeX ()
    leaveCode

      where
        go :: Token -> RWST Env [Output] State m ()
    go tok' :: Token
    tok'@Token{ text :: Token -> Text
    text = Text
    tok } = do
          -- Get the column information before grabbing the token, since
          -- grabbing (possibly) moves the column.
          Int
    col  <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column

          Token -> LaTeX ()
    moveColumnForToken Token
    tok'
          Debug -> Text -> LaTeX ()
    log Debug
    Code Text
    tok

          Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Text -> Bool
    T.null Text
    tok) (RWST Env [Output] State m () -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $
            if (Text -> Bool
    isSpaces Text
    tok) then do
                [Text] -> RWST Env [Output] State m ()
    [Text] -> LaTeX ()
    spaces ([Text] -> RWST Env [Output] State m ())
    -> [Text] -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> [Text]
    T.group (Text -> [Text]) -> Text -> [Text]
    forall a b. (a -> b) -> a -> b
    $ Text -> Text
    replaceSpaces Text
    tok
            else do
              Int -> RWST Env [Output] State m ()
    forall {m :: * -> *} {a}.
    (Eq a, Num a, MonadLogLaTeX m) =>
    a -> RWST Env [Output] State m ()
    ptOpenWhenColumnZero Int
    col
              Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text (Text -> Output) -> Text -> Output
    forall a b. (a -> b) -> a -> b
    $
                -- we return the escaped token wrapped in commands corresponding
                -- to its aspect (if any) and other aspects (e.g. error, unsolved meta)
                ([Char] -> Text -> Text) -> Text -> [[Char]] -> Text
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\[Char]
    c Text
    t -> Text
    cmdPrefix Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Text
    T.pack [Char]
    c Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text -> Text
    cmdArg Text
    t)
                      (Text -> Text
    escape Text
    tok)
                      ([[Char]] -> Text) -> [[Char]] -> Text
    forall a b. (a -> b) -> a -> b
    $ (OtherAspect -> [Char]) -> [OtherAspect] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map OtherAspect -> [Char]
    fromOtherAspect (Set OtherAspect -> [OtherAspect]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList (Set OtherAspect -> [OtherAspect])
    -> Set OtherAspect -> [OtherAspect]
    forall a b. (a -> b) -> a -> b
    $ Aspects -> Set OtherAspect
    otherAspects (Aspects -> Set OtherAspect) -> Aspects -> Set OtherAspect
    forall a b. (a -> b) -> a -> b
    $ Token -> Aspects
    info Token
    tok') [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++
                        (Aspect -> [[Char]]) -> [Aspect] -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Aspect -> [[Char]]
    fromAspect (Maybe Aspect -> [Aspect]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList (Maybe Aspect -> [Aspect]) -> Maybe Aspect -> [Aspect]
    forall a b. (a -> b) -> a -> b
    $ Aspects -> Maybe Aspect
    aspect (Aspects -> Maybe Aspect) -> Aspects -> Maybe Aspect
    forall a b. (a -> b) -> a -> b
    $ Token -> Aspects
    info Token
    tok')

        -- Non-whitespace tokens at the start of a line trigger an
        -- alignment column.
        ptOpenWhenColumnZero :: a -> RWST Env [Output] State m ()
    ptOpenWhenColumnZero a
    col =
            Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (a
    col a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    0) (RWST Env [Output] State m () -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ do
              RWST Env [Output] State m ()
    LaTeX ()
    registerColumnZero
              -- ASR (2021-02-07). The eta-expansion @\o -> output o@ is
              -- required by GHC >= 9.0.1 (see Issue #4955).
              (\Output
    o -> Output -> LaTeX ()
    output Output
    o)(Output -> RWST Env [Output] State m ())
    -> (AlignmentColumn -> Output)
    -> AlignmentColumn
    -> RWST Env [Output] State m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Output
    Text (Text -> Output)
    -> (AlignmentColumn -> Text) -> AlignmentColumn -> Output
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AlignmentColumn -> Text
    ptOpen (AlignmentColumn -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m AlignmentColumn
    -> RWST Env [Output] State m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< RWST Env [Output] State m AlignmentColumn
    LaTeX AlignmentColumn
    columnZero

        -- Translation from OtherAspect to command strings. So far it happens
        -- to correspond to @show@ but it does not have to (cf. fromAspect)
        fromOtherAspect :: OtherAspect -> String
        fromOtherAspect :: OtherAspect -> [Char]
    fromOtherAspect = OtherAspect -> [Char]
    forall a. Show a => a -> [Char]
    show

        fromAspect :: Aspect -> [String]
        fromAspect :: Aspect -> [[Char]]
    fromAspect Aspect
    a = let s :: [[Char]]
    s = [Aspect -> [Char]
    forall a. Show a => a -> [Char]
    show Aspect
    a] in case Aspect
    a of
          Aspect
    Comment           -> [[Char]]
    s
          Aspect
    Keyword           -> [[Char]]
    s
          Aspect
    Hole              -> [[Char]]
    s
          Aspect
    String            -> [[Char]]
    s
          Aspect
    Number            -> [[Char]]
    s
          Aspect
    Symbol            -> [[Char]]
    s
          Aspect
    PrimitiveType     -> [[Char]]
    s
          Aspect
    Pragma            -> [[Char]]
    s
          Aspect
    Background        -> [[Char]]
    s
          Aspect
    Markup            -> [[Char]]
    s
          Name Maybe NameKind
    Nothing Bool
    isOp -> Aspect -> [[Char]]
    fromAspect (Maybe NameKind -> Bool -> Aspect
    Name (NameKind -> Maybe NameKind
    forall a. a -> Maybe a
    Just NameKind
    Postulate) Bool
    isOp)
            -- At the time of writing the case above can be encountered in
            -- --only-scope-checking mode, for instance for the token "Size"
            -- in the following code:
            --
            --   {-# BUILTIN SIZE Size #-}
            --
            -- The choice of "Postulate" works for this example, but might
            -- be less appropriate for others.
          Name (Just NameKind
    kind) Bool
    isOp ->
            (\[Char]
    c -> if Bool
    isOp then [[Char]
    "Operator", [Char]
    c] else [[Char]
    c]) ([Char] -> [[Char]]) -> [Char] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $
            case NameKind
    kind of
              NameKind
    Bound                     -> [Char]
    sk
              NameKind
    Generalizable             -> [Char]
    sk
              Constructor Induction
    Inductive     -> [Char]
    "InductiveConstructor"
              Constructor Induction
    CoInductive   -> [Char]
    "CoinductiveConstructor"
              NameKind
    Datatype                  -> [Char]
    sk
              NameKind
    Field                     -> [Char]
    sk
              NameKind
    Function                  -> [Char]
    sk
              NameKind
    Module                    -> [Char]
    sk
              NameKind
    Postulate                 -> [Char]
    sk
              NameKind
    Primitive                 -> [Char]
    sk
              NameKind
    Record                    -> [Char]
    sk
              NameKind
    Argument                  -> [Char]
    sk
              NameKind
    Macro                     -> [Char]
    sk
            where
            sk :: [Char]
    sk = NameKind -> [Char]
    forall a. Show a => a -> [Char]
    show NameKind
    kind

    -- | Escapes special characters.
    escape :: Text -> Text
    escape :: Text -> Text
    escape (Text -> Maybe (Char, Text)
    T.uncons -> Maybe (Char, Text)
    Nothing)     = Text
    T.empty
    escape (Text -> Maybe (Char, Text)
    T.uncons -> Just (Char
    c, Text
    s)) = [Char] -> Text
    T.pack (Char -> [Char]
    replace Char
    c) Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text -> Text
    escape Text
    s
      where
      replace :: Char -> String
      replace :: Char -> [Char]
    replace Char
    char = case Char
    char of
        Char
    '_'  -> [Char]
    "\\AgdaUnderscore{}"
        Char
    '{'  -> [Char]
    "\\{"
        Char
    '}'  -> [Char]
    "\\}"
        Char
    '#'  -> [Char]
    "\\#"
        Char
    '$'  -> [Char]
    "\\$"
        Char
    '&'  -> [Char]
    "\\&"
        Char
    '%'  -> [Char]
    "\\%"
        Char
    '~'  -> [Char]
    "\\textasciitilde{}"
        Char
    '^'  -> [Char]
    "\\textasciicircum{}"
        Char
    '\\' -> [Char]
    "\\textbackslash{}"
        Char
    ' '  -> [Char]
    "\\ "
        Char
    _    -> [ Char
    char ]
    #if __GLASGOW_HASKELL__ < 810
    escape _                         = __IMPOSSIBLE__
    #endif

    -- | Every element in the list should consist of either one or more
    -- newline characters, or one or more space characters. Two adjacent
    -- list elements must not contain the same character.
    --
    -- If the final element of the list consists of spaces, then these
    -- spaces are assumed to not be trailing whitespace.
    spaces :: [Text] -> LaTeX ()
    spaces :: [Text] -> LaTeX ()
    spaces [] = () -> RWST Env [Output] State m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- Newlines.
    spaces (s :: Text
    s@(Text -> Maybe (Char, Text)
    T.uncons -> Just (Char
    '\n', Text
    _)) : [Text]
    ss) = do
      Int
    col <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column
      Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    col Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0) (RWST Env [Output] State m () -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $
        -- ASR (2021-02-07). The eta-expansion @\o -> output o@ is
        -- required by GHC >= 9.0.1 (see Issue #4955).
        (\Output
    o -> Output -> LaTeX ()
    output Output
    o) (Output -> RWST Env [Output] State m ())
    -> (AlignmentColumn -> Output)
    -> AlignmentColumn
    -> RWST Env [Output] State m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Output
    Text (Text -> Output)
    -> (AlignmentColumn -> Text) -> AlignmentColumn -> Output
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AlignmentColumn -> Text
    ptOpen (AlignmentColumn -> RWST Env [Output] State m ())
    -> RWST Env [Output] State m AlignmentColumn
    -> RWST Env [Output] State m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< RWST Env [Output] State m AlignmentColumn
    LaTeX AlignmentColumn
    columnZero
      Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text (Text -> Output) -> Text -> Output
    forall a b. (a -> b) -> a -> b
    $ Text
    ptClose Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ptNL Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>
                      Int -> Text -> Text
    T.replicate (TextWidthEstimator
    T.length Text
    s Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Text
    ptEmptyLine
      RWST Env [Output] State m ()
    LaTeX ()
    resetColumn
      [Text] -> LaTeX ()
    spaces [Text]
    ss

    -- Spaces followed by a newline character.
    spaces (Text
    _ : ss :: [Text]
    ss@(Text
    _ : [Text]
    _)) = [Text] -> LaTeX ()
    spaces [Text]
    ss

    -- Spaces that are not followed by a newline character.
    spaces [ Text
    s ] = do
      Int
    col <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column

      let len :: Int
    len  = TextWidthEstimator
    T.length Text
    s
          kind :: Kind
    kind = if Int
    col Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    0 Bool -> Bool -> Bool
    && Int
    len Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1
                 then Kind
    Indentation
                 else Kind
    Alignment

      Int -> LaTeX ()
    moveColumn Int
    len
      AlignmentColumn
    column <- Kind -> LaTeX AlignmentColumn
    registerColumn Kind
    kind

      if Int
    col Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    0
      then Debug -> Text -> LaTeX ()
    log Debug
    Spaces Text
    "col /= 0"
      else do
        [AlignmentColumn]
    columns    <- (State -> [AlignmentColumn])
    -> RWST Env [Output] State m [AlignmentColumn]
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> [AlignmentColumn]
    columnsPrev
        Int
    codeBlock  <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    codeBlock

        Debug -> Text -> LaTeX ()
    log Debug
    Spaces (Text -> RWST Env [Output] State m ())
    -> Text -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $
          Text
    "col == 0: " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Text
    T.pack ((Int, [AlignmentColumn]) -> [Char]
    forall a. Show a => a -> [Char]
    show (Int
    len, [AlignmentColumn]
    columns))

        case (AlignmentColumn -> Bool) -> [AlignmentColumn] -> [AlignmentColumn]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    len) (Int -> Bool)
    -> (AlignmentColumn -> Int) -> AlignmentColumn -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AlignmentColumn -> Int
    columnColumn) [AlignmentColumn]
    columns of
          AlignmentColumn
    c : [AlignmentColumn]
    _ | AlignmentColumn -> Int
    columnColumn AlignmentColumn
    c Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    len, Maybe Int -> Bool
    forall a. Maybe a -> Bool
    isJust (AlignmentColumn -> Maybe Int
    columnKind AlignmentColumn
    c) -> do
            -- Align. (This happens automatically if the column is an
            -- alignment column, but c is an indentation column.)
            AlignmentColumn -> LaTeX ()
    useColumn AlignmentColumn
    c
            Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text (Text -> Output) -> Text -> Output
    forall a b. (a -> b) -> a -> b
    $ Text
    ptOpenBeginningOfLine
            Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text (Text -> Output) -> Text -> Output
    forall a b. (a -> b) -> a -> b
    $ AlignmentColumn -> Text
    ptClose' AlignmentColumn
    c
          AlignmentColumn
    c : [AlignmentColumn]
    _ | AlignmentColumn -> Int
    columnColumn AlignmentColumn
    c Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <  Int
    len -> do
            -- Indent.
            AlignmentColumn -> LaTeX ()
    useColumn AlignmentColumn
    c
            Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text (Text -> Output) -> Text -> Output
    forall a b. (a -> b) -> a -> b
    $ AlignmentColumn -> Int -> Text
    ptOpenIndent AlignmentColumn
    c (Int
    codeBlock Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - AlignmentColumn -> Int
    columnCodeBlock AlignmentColumn
    c)
          [AlignmentColumn]
    _ -> () -> RWST Env [Output] State m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      Output -> RWST Env [Output] State m ()
    Output -> LaTeX ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ AlignmentColumn -> Output
    MaybeColumn AlignmentColumn
    column

    -- | Split multi-lines string literals into multiple string literals
    -- Isolating leading spaces for the alignment machinery to work
    -- properly
    stringLiteral :: Token -> Tokens
    stringLiteral :: Token -> [Token]
    stringLiteral Token
    t | Aspects -> Maybe Aspect
    aspect (Token -> Aspects
    info Token
    t) Maybe Aspect -> Maybe Aspect -> Bool
    forall a. Eq a => a -> a -> Bool
    == Aspect -> Maybe Aspect
    forall a. a -> Maybe a
    Just Aspect
    String =
      (Text -> Token) -> [Text] -> [Token]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Text
    x -> Token
    t { text :: Text
    text = Text
    x })
              ([Text] -> [Token]) -> [Text] -> [Token]
    forall a b. (a -> b) -> a -> b
    $ (Text -> [Text]) -> [Text] -> [Text]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Text -> [Text]
    leadingSpaces
              ([Text] -> [Text]) -> [Text] -> [Text]
    forall a b. (a -> b) -> a -> b
    $ Text -> [Text] -> [Text]
    forall a. a -> [a] -> [a]
    List.intersperse Text
    "\n"
              ([Text] -> [Text]) -> [Text] -> [Text]
    forall a b. (a -> b) -> a -> b
    $ Text -> [Text]
    T.lines (Token -> Text
    text Token
    t)
      where
      leadingSpaces :: Text -> [Text]
      leadingSpaces :: Text -> [Text]
    leadingSpaces Text
    tok = [Text
    pre, Text
    suf]
        where (Text
    pre , Text
    suf) = (Char -> Bool) -> Text -> (Text, Text)
    T.span Char -> Bool
    isSpaceNotNewline Text
    tok

    stringLiteral Token
    t = [Token
    t]

    -- | Split multi-line comments into several tokens.
    -- See issue #5398.
    multiLineComment :: Token -> Tokens
    multiLineComment :: Token -> [Token]
    multiLineComment Token{ text :: Token -> Text
    text = Text
    s, info :: Token -> Aspects
    info = Aspects
    i } | Aspects -> Maybe Aspect
    aspect Aspects
    i Maybe Aspect -> Maybe Aspect -> Bool
    forall a. Eq a => a -> a -> Bool
    == Aspect -> Maybe Aspect
    forall a. a -> Maybe a
    Just Aspect
    Comment =
      (Text -> Token) -> [Text] -> [Token]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> Aspects -> Token
    `Token` Aspects
    i)
        ([Text] -> [Token]) -> [Text] -> [Token]
    forall a b. (a -> b) -> a -> b
    $ Text -> [Text] -> [Text]
    forall a. a -> [a] -> [a]
    List.intersperse Text
    "\n"
        ([Text] -> [Text]) -> [Text] -> [Text]
    forall a b. (a -> b) -> a -> b
    $ Text -> [Text]
    T.lines Text
    s
    -- multiLineComment Token{ text = s, info = i } | aspect i == Just Comment =
    --   map emptyToPar
    --     $ List1.groupBy ((==) `on` T.null)
    --     $ T.lines s
    --   where
    --   emptyToPar :: List1 Text -> Token
    --   emptyToPar ts@(t :| _)
    --     | T.null t  = Token{ text = "\n", info = mempty }
    --     | otherwise = Token{ text = sconcat $ List1.intersperse "\n" ts, info = i }
    multiLineComment Token
    t = [Token
    t]

    ------------------------------------------------------------------------
    -- * Main.

    -- | The Agda data directory containing the files for the LaTeX backend.

    latexDataDir :: FilePath
    latexDataDir :: [Char]
    latexDataDir = [Char]
    "latex"

    defaultStyFile :: String
    defaultStyFile :: [Char]
    defaultStyFile = [Char]
    "agda.sty"

    data LaTeXOptions = LaTeXOptions
      { LaTeXOptions -> [Char]
    latexOptOutDir         :: FilePath
      , LaTeXOptions -> Maybe AbsolutePath
    latexOptSourceFileName :: Maybe AbsolutePath
        -- ^ 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.
      , LaTeXOptions -> Bool
    latexOptCountClusters  :: Bool
        -- ^ Count extended grapheme clusters rather than code points when
        -- generating LaTeX.
      }

    getTextWidthEstimator :: Bool -> TextWidthEstimator
    getTextWidthEstimator :: Bool -> TextWidthEstimator
    getTextWidthEstimator Bool
    _countClusters =
    #ifdef COUNT_CLUSTERS
      if _countClusters
        then length . (ICU.breaks (ICU.breakCharacter ICU.Root))
        else T.length
    #else
      TextWidthEstimator
    T.length
    #endif

    -- | Create the common base output directory and check for/install the style file.
    prepareCommonAssets :: (MonadLogLaTeX m, MonadIO m) => FilePath -> m ()
    prepareCommonAssets :: forall (m :: * -> *).
    (MonadLogLaTeX m, MonadIO m) =>
    [Char] -> m ()
    prepareCommonAssets [Char]
    dir = do
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> [Char] -> IO ()
    createDirectoryIfMissing Bool
    True [Char]
    dir
      (ExitCode
    code, [Char]
    _, [Char]
    _) <-
        IO (ExitCode, [Char], [Char]) -> m (ExitCode, [Char], [Char])
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (ExitCode, [Char], [Char]) -> m (ExitCode, [Char], [Char]))
    -> IO (ExitCode, [Char], [Char]) -> m (ExitCode, [Char], [Char])
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [[Char]] -> [Char] -> IO (ExitCode, [Char], [Char])
    readProcessWithExitCode
            [Char]
    "kpsewhich"
            [[Char]
    "--path=" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    dir, [Char]
    defaultStyFile]
            [Char]
    ""
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (ExitCode
    code ExitCode -> ExitCode -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ExitCode
    ExitSuccess) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        LogMessage -> m ()
    forall (m :: * -> *). MonadLogLaTeX m => LogMessage -> m ()
    logLaTeX (LogMessage -> m ()) -> LogMessage -> m ()
    forall a b. (a -> b) -> a -> b
    $ Debug -> Text -> [Text] -> LogMessage
    LogMessage Debug
    FileSystem
          ([Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords [[Char]
    defaultStyFile, [Char]
    "was not found. Copying a default version of", [Char]
    defaultStyFile, [Char]
    "into", [Char]
    dir])
          []
        IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char]
    styFile <- [Char] -> IO [Char]
    getDataFileName ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    latexDataDir [Char] -> ShowS
    </> [Char]
    defaultStyFile
          [Char] -> [Char] -> IO ()
    copyFile [Char]
    styFile ([Char]
    dir [Char] -> ShowS
    </> [Char]
    defaultStyFile)

    -- | Generates a LaTeX file for the given interface.
    generateLaTeXIO :: (MonadLogLaTeX m, MonadIO m) => LaTeXOptions -> Interface -> m ()
    generateLaTeXIO :: forall (m :: * -> *).
    (MonadLogLaTeX m, MonadIO m) =>
    LaTeXOptions -> Interface -> m ()
    generateLaTeXIO LaTeXOptions
    opts Interface
    i = do
      let textWidthEstimator :: TextWidthEstimator
    textWidthEstimator = Bool -> TextWidthEstimator
    getTextWidthEstimator (LaTeXOptions -> Bool
    latexOptCountClusters LaTeXOptions
    opts)
      let baseDir :: [Char]
    baseDir = LaTeXOptions -> [Char]
    latexOptOutDir LaTeXOptions
    opts
      let outPath :: [Char]
    outPath = [Char]
    baseDir [Char] -> ShowS
    </> (TopLevelModuleName -> [Char]
    latexOutRelativeFilePath (TopLevelModuleName -> [Char]) -> TopLevelModuleName -> [Char]
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TopLevelModuleName
    toTopLevelModuleName (ModuleName -> TopLevelModuleName)
    -> ModuleName -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ Interface -> ModuleName
    iModuleName Interface
    i)
      ByteString
    latex <- Text -> ByteString
    E.encodeUtf8 (Text -> ByteString) -> m Text -> m ByteString
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Env -> Maybe AbsolutePath -> Text -> HighlightingInfo -> m Text
    forall (m :: * -> *).
    MonadLogLaTeX m =>
    Env -> Maybe AbsolutePath -> Text -> HighlightingInfo -> m Text
    toLaTeX
                  (TextWidthEstimator -> Env
    emptyEnv TextWidthEstimator
    textWidthEstimator)
                  (LaTeXOptions -> Maybe AbsolutePath
    latexOptSourceFileName LaTeXOptions
    opts)
                  (Interface -> Text
    iSource Interface
    i)
                  (Interface -> HighlightingInfo
    iHighlighting Interface
    i)
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        Bool -> [Char] -> IO ()
    createDirectoryIfMissing Bool
    True (ShowS
    takeDirectory [Char]
    outPath)
        [Char] -> ByteString -> IO ()
    BS.writeFile [Char]
    outPath ByteString
    latex

    latexOutRelativeFilePath :: TopLevelModuleName -> FilePath
    latexOutRelativeFilePath :: TopLevelModuleName -> [Char]
    latexOutRelativeFilePath TopLevelModuleName
    m = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char
    pathSeparator] (NonEmpty [Char] -> [[Char]]
    forall a. NonEmpty a -> [a]
    List1.toList (NonEmpty [Char] -> [[Char]]) -> NonEmpty [Char] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> NonEmpty [Char]
    moduleNameParts TopLevelModuleName
    m) [Char] -> ShowS
    <.> [Char]
    "tex"

    groupByFst :: forall a b. Eq a => [(a,b)] -> [(a,[b])]
    groupByFst :: forall a b. Eq a => [(a, b)] -> [(a, [b])]
    groupByFst =
        ([(a, b)] -> (a, [b])) -> [[(a, b)]] -> [(a, [b])]
    forall a b. (a -> b) -> [a] -> [b]
    map (\[(a, b)]
    xs -> case [(a, b)]
    xs of                     -- Float the grouping to the top level
              []           -> (a, [b])
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              (a
    tag, b
    _): [(a, b)]
    _ -> (a
    tag, ((a, b) -> b) -> [(a, b)] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map (a, b) -> b
    forall a b. (a, b) -> b
    snd [(a, b)]
    xs))

      ([[(a, b)]] -> [(a, [b])])
    -> ([(a, b)] -> [[(a, b)]]) -> [(a, b)] -> [(a, [b])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((a, b) -> (a, b) -> Bool) -> [(a, b)] -> [[(a, b)]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    List.groupBy (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (a -> a -> Bool) -> ((a, b) -> a) -> (a, b) -> (a, b) -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (a, b) -> a
    forall a b. (a, b) -> a
    fst)  -- Group together characters in the same
                                      -- role.

    -- | Transforms the source code into LaTeX.
    toLaTeX
      :: MonadLogLaTeX m
      => Env
      -> Maybe AbsolutePath
      -> L.Text
      -> HighlightingInfo
      -> m L.Text
    toLaTeX :: forall (m :: * -> *).
    MonadLogLaTeX m =>
    Env -> Maybe AbsolutePath -> Text -> HighlightingInfo -> m Text
    toLaTeX Env
    env Maybe AbsolutePath
    path Text
    source HighlightingInfo
    hi =

      Env -> [(LayerRole, [Token])] -> m Text
    forall (m :: * -> *).
    MonadLogLaTeX m =>
    Env -> [(LayerRole, [Token])] -> m Text
    processTokens Env
    env

        ([(LayerRole, [Token])] -> m Text)
    -> ([Char] -> [(LayerRole, [Token])]) -> [Char] -> m Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((LayerRole, [(Maybe Aspects, Char)]) -> (LayerRole, [Token]))
    -> [(LayerRole, [(Maybe Aspects, Char)])] -> [(LayerRole, [Token])]
    forall a b. (a -> b) -> [a] -> [b]
    map
          ( ( \(LayerRole
    role, [Token]
    tokens) ->
                (LayerRole
    role,) ([Token] -> (LayerRole, [Token]))
    -> [Token] -> (LayerRole, [Token])
    forall a b. (a -> b) -> a -> b
    $
                  -- This bit fixes issue 954
                  ( Bool -> ([Token] -> [Token]) -> [Token] -> [Token]
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (LayerRole -> Bool
    L.isCode LayerRole
    role) (([Token] -> [Token]) -> [Token] -> [Token])
    -> ([Token] -> [Token]) -> [Token] -> [Token]
    forall a b. (a -> b) -> a -> b
    $
                      -- Remove trailing whitespace from the
                      -- final line; the function spaces
                      -- expects trailing whitespace to be
                      -- followed by a newline character.
                        ([Token] -> [Token]) -> [Token] -> [Token]
    forall a. ([a] -> [a]) -> [a] -> [a]
    whenMoreThanOne
                          ( (Token -> Token) -> [Token] -> [Token]
    forall a. (a -> a) -> [a] -> [a]
    updateLast
                              ((Token -> Token) -> [Token] -> [Token])
    -> (Token -> Token) -> [Token] -> [Token]
    forall a b. (a -> b) -> a -> b
    $ (Text -> Text) -> Token -> Token
    withTokenText
                              ((Text -> Text) -> Token -> Token)
    -> (Text -> Text) -> Token -> Token
    forall a b. (a -> b) -> a -> b
    $ \Text
    suf ->
                                Text -> (Text -> Text) -> Maybe Text -> Text
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe
                                  Text
    suf
                                  ((Char -> Bool) -> Text -> Text
    T.dropWhileEnd Char -> Bool
    isSpaceNotNewline)
                                  (Text -> Text -> Maybe Text
    T.stripSuffix Text
    "\n" Text
    suf)
                          )
                          ([Token] -> [Token]) -> ([Token] -> [Token]) -> [Token] -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Token -> Token) -> [Token] -> [Token]
    forall a. (a -> a) -> [a] -> [a]
    updateLast ((Text -> Text) -> Token -> Token
    withTokenText ((Text -> Text) -> Token -> Token)
    -> (Text -> Text) -> Token -> Token
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> Text -> Text
    T.dropWhileEnd Char -> Bool
    isSpaceNotNewline)
                          ([Token] -> [Token]) -> ([Token] -> [Token]) -> [Token] -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Token -> Token) -> [Token] -> [Token]
    forall a. (a -> a) -> [a] -> [a]
    updateHead
                            ( (Text -> Text) -> Token -> Token
    withTokenText ((Text -> Text) -> Token -> Token)
    -> (Text -> Text) -> Token -> Token
    forall a b. (a -> b) -> a -> b
    $
                                \Text
    pre ->
                                  Text -> Maybe Text -> Text
    forall a. a -> Maybe a -> a
    fromMaybe Text
    pre (Maybe Text -> Text) -> Maybe Text -> Text
    forall a b. (a -> b) -> a -> b
    $ Text -> Text -> Maybe Text
    T.stripPrefix Text
    "\n" (Text -> Maybe Text) -> Text -> Maybe Text
    forall a b. (a -> b) -> a -> b
    $
                                    (Char -> Bool) -> Text -> Text
    T.dropWhile
                                      Char -> Bool
    isSpaceNotNewline
                                      Text
    pre
                            )
                  )
                    [Token]
    tokens
            ) ((LayerRole, [Token]) -> (LayerRole, [Token]))
    -> ((LayerRole, [(Maybe Aspects, Char)]) -> (LayerRole, [Token]))
    -> (LayerRole, [(Maybe Aspects, Char)])
    -> (LayerRole, [Token])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ( ([(Maybe Aspects, Char)] -> [Token])
    -> (LayerRole, [(Maybe Aspects, Char)]) -> (LayerRole, [Token])
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second
                    ( -- Split tokens at newlines
                      (Token -> [Token]) -> [Token] -> [Token]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Token -> [Token]
    stringLiteral
                    ([Token] -> [Token])
    -> ([(Maybe Aspects, Char)] -> [Token])
    -> [(Maybe Aspects, Char)]
    -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Token -> [Token]) -> [Token] -> [Token]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Token -> [Token]
    multiLineComment
                    ([Token] -> [Token])
    -> ([(Maybe Aspects, Char)] -> [Token])
    -> [(Maybe Aspects, Char)]
    -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Maybe Aspects, [Char]) -> Token)
    -> [(Maybe Aspects, [Char])] -> [Token]
    forall a b. (a -> b) -> [a] -> [b]
    map ( \(Maybe Aspects
    mi, [Char]
    cs) ->
                                  Token :: Text -> Aspects -> Token
    Token {text :: Text
    text = [Char] -> Text
    T.pack [Char]
    cs, info :: Aspects
    info = Aspects -> Maybe Aspects -> Aspects
    forall a. a -> Maybe a -> a
    fromMaybe Aspects
    forall a. Monoid a => a
    mempty Maybe Aspects
    mi}
                          )
                    ([(Maybe Aspects, [Char])] -> [Token])
    -> ([(Maybe Aspects, Char)] -> [(Maybe Aspects, [Char])])
    -> [(Maybe Aspects, Char)]
    -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Maybe Aspects, Char)] -> [(Maybe Aspects, [Char])]
    forall a b. Eq a => [(a, b)] -> [(a, [b])]
    groupByFst
                    )
                )
          )
        ([(LayerRole, [(Maybe Aspects, Char)])] -> [(LayerRole, [Token])])
    -> ([Char] -> [(LayerRole, [(Maybe Aspects, Char)])])
    -> [Char]
    -> [(LayerRole, [Token])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(LayerRole, (Maybe Aspects, Char))]
    -> [(LayerRole, [(Maybe Aspects, Char)])]
    forall a b. Eq a => [(a, b)] -> [(a, [b])]
    groupByFst

      -- Look up the meta info at each position in the highlighting info.
      ([(LayerRole, (Maybe Aspects, Char))]
     -> [(LayerRole, [(Maybe Aspects, Char)])])
    -> ([Char] -> [(LayerRole, (Maybe Aspects, Char))])
    -> [Char]
    -> [(LayerRole, [(Maybe Aspects, Char)])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> (LayerRole, Char) -> (LayerRole, (Maybe Aspects, Char)))
    -> [Int]
    -> [(LayerRole, Char)]
    -> [(LayerRole, (Maybe Aspects, Char))]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\Int
    pos (LayerRole
    role, Char
    char) -> (LayerRole
    role, (Int -> IntMap Aspects -> Maybe Aspects
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    pos IntMap Aspects
    infoMap, Char
    char)))
                [Int
    1..] ([(LayerRole, Char)] -> [(LayerRole, (Maybe Aspects, Char))])
    -> ([Char] -> [(LayerRole, Char)])
    -> [Char]
    -> [(LayerRole, (Maybe Aspects, Char))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . -- Add position in file to each character.
                  -- Map each character to its role
                  Layers -> [(LayerRole, Char)]
    atomizeLayers (Layers -> [(LayerRole, Char)])
    -> ([Char] -> Layers) -> [Char] -> [(LayerRole, Char)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Position -> [Char] -> Layers
    literateTeX (Maybe AbsolutePath -> Position
    startPos Maybe AbsolutePath
    path)

      ([Char] -> m Text) -> [Char] -> m Text
    forall a b. (a -> b) -> a -> b
    $ Text -> [Char]
    L.unpack Text
    source
      where
      infoMap :: IntMap Aspects
    infoMap = HighlightingInfo -> IntMap Aspects
    forall a m. IsBasicRangeMap a m => m -> IntMap a
    toMap HighlightingInfo
    hi

      whenMoreThanOne :: ([a] -> [a]) -> [a] -> [a]
      whenMoreThanOne :: forall a. ([a] -> [a]) -> [a] -> [a]
    whenMoreThanOne [a] -> [a]
    f xs :: [a]
    xs@(a
    _:a
    _:[a]
    _) = [a] -> [a]
    f [a]
    xs
      whenMoreThanOne [a] -> [a]
    _ [a]
    xs         = [a]
    xs

    processTokens
      :: MonadLogLaTeX m
      => Env
      -> [(LayerRole, Tokens)]
      -> m L.Text
    processTokens :: forall (m :: * -> *).
    MonadLogLaTeX m =>
    Env -> [(LayerRole, [Token])] -> m Text
    processTokens Env
    env [(LayerRole, [Token])]
    ts = do
      ((), State
    s, [Output]
    os) <- LaTeX () -> Env -> State -> m ((), State, [Output])
    forall (m :: * -> *) a.
    MonadLogLaTeX m =>
    LaTeX a -> Env -> State -> m (a, State, [Output])
    runLaTeX ([(LayerRole, [Token])] -> LaTeX ()
    processLayers [(LayerRole, [Token])]
    ts) Env
    env State
    emptyState
      Text -> m Text
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> m Text) -> Text -> m Text
    forall a b. (a -> b) -> a -> b
    $ [Text] -> Text
    L.fromChunks ([Text] -> Text) -> [Text] -> Text
    forall a b. (a -> b) -> a -> b
    $ (Output -> Text) -> [Output] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    map (State -> Output -> Text
    render State
    s) [Output]
    os
      where
        render :: State -> Output -> Text
    render State
    _ (Text Text
    s)        = Text
    s
        render State
    s (MaybeColumn AlignmentColumn
    c)
          | Just Int
    i <- AlignmentColumn -> Maybe Int
    columnKind AlignmentColumn
    c,
            Bool -> Bool
    not (Int
    i Int -> HashSet Int -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    `Set.member` State -> HashSet Int
    usedColumns State
    s) = Text
    agdaSpace
          | Bool
    otherwise                          = Text
    nl Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> AlignmentColumn -> Text
    ptOpen AlignmentColumn
    c