    {-# LANGUAGE CPP #-}

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

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

    import Prelude hiding (log)

    import Data.Bifunctor (second)
    import Data.Char
    import Data.Maybe
    import Data.Function (on)
    import Data.Foldable (toList)

    import Control.Exception.Base (IOException, try)
    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.FilePath
    import System.Process ( readProcess )

    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 Agda.Syntax.Common
    import Agda.Syntax.Parser.Literate (literateTeX, LayerRole, atomizeLayers)
    import qualified Agda.Syntax.Parser.Literate as L
    import Agda.Syntax.Position (RangeFile, startPos')
    import Agda.Syntax.TopLevelModuleName
      (TopLevelModuleName, moduleNameParts)

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

    import Agda.TypeChecking.Monad (Interface(..)) --, reportSLn)

    import Agda.Setup ( getDataFileName )

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

    import Agda.Utils.Impossible

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

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

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

    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
    $cshowsPrec :: Int -> LogMessage -> ShowS
    showsPrec :: Int -> LogMessage -> ShowS
    $cshow :: LogMessage -> [Char]
    show :: LogMessage -> [Char]
    $cshowList :: [LogMessage] -> ShowS
    showList :: [LogMessage] -> ShowS
    Show

    ------------------------------------------------------------------------
    -- * The monad and its associated data types.

    -- | The @LaTeX@ monad is a combination of @RWST@ and a logger @m@.
    --
    -- The reader part contains static options used,
    -- the writer is where the output goes,
    -- 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 LaTeXT = RWST Env [Output] State
    type LaTeX a = forall m. MonadLogLaTeX m => LaTeXT m a
    -- Andreas, 2025-03-23 we sometimes expand @a -> LaTeX b@
    -- to @forall m. MonadLogLaTeX m => a -> LaTeXT m b@
    -- to combat changes in the type checker of GHC 9 over GHC 8.
    -- Originally (by asr, 2021-02-07) we used eta-expansions in these places
    -- to circumvent the GHC type checker regressions (see Issue #4955).

    -- | Output items.

    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
    $cshowsPrec :: Int -> Output -> ShowS
    showsPrec :: Int -> Output -> ShowS
    $cshow :: Output -> [Char]
    show :: Output -> [Char]
    $cshowList :: [Output] -> ShowS
    showList :: [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
    $c== :: Kind -> Kind -> Bool
    == :: Kind -> Kind -> Bool
    $c/= :: Kind -> Kind -> Bool
    /= :: 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
    $cshowsPrec :: Int -> Kind -> ShowS
    showsPrec :: Int -> Kind -> ShowS
    $cshow :: Kind -> [Char]
    show :: Kind -> [Char]
    $cshowList :: [Kind] -> ShowS
    showList :: [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
    $cshowsPrec :: Int -> AlignmentColumn -> ShowS
    showsPrec :: Int -> AlignmentColumn -> ShowS
    $cshow :: AlignmentColumn -> [Char]
    show :: AlignmentColumn -> [Char]
    $cshowList :: [AlignmentColumn] -> ShowS
    showList :: [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
    $cshowsPrec :: Int -> Token -> ShowS
    showsPrec :: Int -> Token -> ShowS
    $cshow :: Token -> [Char]
    show :: Token -> [Char]
    $cshowList :: [Token] -> ShowS
    showList :: [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 = f 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
    $c== :: Debug -> Debug -> Bool
    == :: Debug -> Debug -> Bool
    $c/= :: Debug -> Debug -> Bool
    /= :: 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
    $cshowsPrec :: Int -> Debug -> ShowS
    showsPrec :: Int -> Debug -> ShowS
    $cshow :: Debug -> [Char]
    show :: Debug -> [Char]
    $cshowList :: [Debug] -> ShowS
    showList :: [Debug] -> ShowS
    Show)

    -- | Run function for the @LaTeX@ monad.
    runLaTeX :: MonadLogLaTeX m =>
      LaTeXT m a -> Env -> State -> m (a, State, [Output])
    runLaTeX :: forall (m :: * -> *) a.
    MonadLogLaTeX m =>
    LaTeXT m a -> Env -> State -> m (a, State, [Output])
    runLaTeX = 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

    emptyState :: State
    emptyState :: State
    emptyState = 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Text -> Bool
    isSpaces Text
    t) do
        Debug -> Text -> LaTeX ()
    log Debug
    MoveColumn Text
    t
        Int -> RWST Env [Output] State m ()
    forall (m :: * -> *). MonadLogLaTeX m => Int -> LaTeXT m ()
    moveColumn (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
    =<< Text -> LaTeX Int
    size Text
    t

    -- | 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      = 0
        , columnsPrev = mergeCols (columns s) (columnsPrev s)
        , 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 :: MonadLogLaTeX m => Int -> LaTeXT m ()
    moveColumn :: forall (m :: * -> *). MonadLogLaTeX m => Int -> LaTeXT m ()
    moveColumn Int
    i = (State -> State) -> RWST Env [Output] State m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify \ State
    s -> State
    s { column = i + column s }

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

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

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

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

    -- | Registers column zero as an alignment column.

    registerColumnZero :: LaTeX ()
    registerColumnZero :: LaTeX ()
    registerColumnZero = do
      c <- LaTeXT m AlignmentColumn
    LaTeX AlignmentColumn
    columnZero
      modify $ \State
    s -> State
    s { columns = [c] }

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

    enterCode :: LaTeX ()
    enterCode :: LaTeX ()
    enterCode = do
      LaTeXT m ()
    LaTeX ()
    resetColumn
      (State -> State) -> LaTeXT m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((State -> State) -> LaTeXT m ())
    -> (State -> State) -> LaTeXT m ()
    forall a b. (a -> b) -> a -> b
    $ \State
    s -> State
    s { codeBlock = codeBlock s + 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 a. a -> RWST Env [Output] State m a
    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 a. [a] -> 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
      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
      when (debug `elem` logLevels) $ do
        lift $ logLaTeX (LogMessage debug text extra)

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

    output :: MonadLogLaTeX m => Output -> LaTeXT m ()
    output :: forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    output Output
    item = do
      Debug -> Text -> LaTeX ()
    log Debug
    Output (Text -> LaTeX ()) -> Text -> LaTeX ()
    forall a b. (a -> b) -> a -> b
    $ Output -> Text
    forall a. Show a => a -> Text
    tshow Output
    item
      [Output] -> LaTeXT 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 :: MonadLogLaTeX m => [(LayerRole, Tokens)] -> LaTeXT m ()
    processLayers :: forall (m :: * -> *).
    MonadLogLaTeX m =>
    [(LayerRole, [Token])] -> LaTeXT m ()
    processLayers = ((LayerRole, [Token]) -> RWST Env [Output] State m ())
    -> [(LayerRole, [Token])] -> RWST Env [Output] State m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ \ (LayerRole
    layerRole, [Token]
    toks) -> do
      case LayerRole
    layerRole of
        LayerRole
    L.Markup  -> [Token] -> RWST Env [Output] State m ()
    forall (m :: * -> *). MonadLogLaTeX m => [Token] -> LaTeXT m ()
    processMarkup  [Token]
    toks
        LayerRole
    L.Comment -> [Token] -> RWST Env [Output] State m ()
    forall (m :: * -> *). MonadLogLaTeX m => [Token] -> LaTeXT m ()
    processComment [Token]
    toks
        LayerRole
    L.Code    -> [Token] -> LaTeX ()
    processCode    [Token]
    toks

    -- | Deals with markup, which is output verbatim.
    processMarkup :: MonadLogLaTeX m => Tokens -> LaTeXT m ()
    processMarkup :: forall (m :: * -> *). MonadLogLaTeX m => [Token] -> LaTeXT m ()
    processMarkup = (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
    t -> do
      Token -> LaTeX ()
    moveColumnForToken Token
    t
      Output -> RWST Env [Output] State m ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    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
    $ Token -> Text
    text Token
    t

    -- | Deals with literate text, which is output verbatim
    processComment :: MonadLogLaTeX m => Tokens -> LaTeXT m ()
    processComment :: forall (m :: * -> *). MonadLogLaTeX m => [Token] -> LaTeXT m ()
    processComment = (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
    t -> do
      let t' :: Text
    t' = Token -> Text
    text Token
    t
      Bool
    -> RWST Env [Output] State m () -> RWST Env [Output] State m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Text
    "%" Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Text -> Text
    T.take Int
    1 (Text -> Text
    T.stripStart 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
        Token -> LaTeX ()
    moveColumnForToken Token
    t
      Output -> RWST Env [Output] State m ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    output (Output -> RWST Env [Output] State m ())
    -> Output -> RWST Env [Output] State m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text Text
    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 -> LaTeXT m ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    output (Output -> LaTeXT m ()) -> Output -> LaTeXT m ()
    forall a b. (a -> b) -> a -> b
    $ Text -> Output
    Text Text
    nl
      LaTeXT m ()
    LaTeX ()
    enterCode
      (Token -> LaTeXT m ()) -> [Token] -> LaTeXT m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Token -> LaTeXT m ()
    forall {m :: * -> *}.
    MonadLogLaTeX m =>
    Token -> RWST Env [Output] State m ()
    go [Token]
    toks'
      Int -> LaTeXT m ()
    forall {m :: * -> *} {a}.
    (Eq a, Num a, MonadLogLaTeX m) =>
    a -> RWST Env [Output] State m ()
    ptOpenWhenColumnZero (Int -> LaTeXT m ())
    -> RWST Env [Output] State m Int -> LaTeXT 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 -> LaTeXT m ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    output (Output -> LaTeXT m ()) -> Output -> LaTeXT 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
      LaTeXT 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.
          col  <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column

          moveColumnForToken tok'
          log Code tok

          unless (T.null tok) $
            if (isSpaces tok) then do
                spaces $ T.group $ replaceSpaces tok
            else do
              ptOpenWhenColumnZero col
              output $ Text $
                -- we return the escaped token wrapped in commands corresponding
                -- to its aspect (if any) and other aspects (e.g. error, unsolved meta)
                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)
                      (escape tok)
                      $ map fromOtherAspect (toList $ otherAspects $ info tok') ++
                        concatMap fromAspect (toList $ aspect $ info 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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
              Output -> RWST Env [Output] State m ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    output (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 a. a -> RWST Env [Output] State m a
    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
      col <- (State -> Int) -> RWST Env [Output] State m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets State -> Int
    column
      when (col == 0) do
        output . Text . ptOpen =<< columnZero
      output $ Text $ ptClose <> ptNL <>
                      T.replicate (T.length s - 1) ptEmptyLine
      resetColumn
      spaces 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
      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  = TextWidthEstimator
    T.length Text
    s
          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

      moveColumn len
      column <- registerColumn kind

      if col /= 0
      then log Spaces "col /= 0"
      else do
        columns    <- gets columnsPrev
        codeBlock  <- gets codeBlock

        log Spaces $
          "col == 0: " <> T.pack (show (len, columns))

        case filter ((<= len) . columnColumn) 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 ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    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 ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    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 ()
    forall (m :: * -> *). MonadLogLaTeX m => Output -> LaTeXT m ()
    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 a. a -> RWST Env [Output] State m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      output $ MaybeColumn 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 = 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 RangeFile
    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.
      , 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
      -- Make sure @dir@ will exist.
      dirExisted <- IO Bool -> m Bool
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesDirectoryExist [Char]
    dir
      unless dirExisted $
        -- Create directory @dir@ and parent directories.
        liftIO $ createDirectoryIfMissing True dir

      -- Check whether TeX will find @agda.sty@.
      texFindsSty <- liftIO $ try $
          readProcess
            "kpsewhich"
            (applyWhen dirExisted (("--path=" ++ dir) :) [defaultStyFile])
            ""
      case texFindsSty of
        Right [Char]
    _ -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Left (IOException
    e :: IOException) -> do
         -- -- we are lacking MonadDebug here, so no debug printing via reportSLn
         -- reportSLn "compile.latex.sty" 70 $ unlines
         --   [ unwords [ "Searching for", defaultStyFile, "in", dir, "returns:" ]
         --   , show e
         --   ]
         let agdaSty :: [Char]
    agdaSty = [Char]
    dir [Char] -> ShowS
    </> [Char]
    defaultStyFile
         m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    dirExisted m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` IO Bool -> m Bool
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ([Char] -> IO Bool
    doesFileExist [Char]
    agdaSty)) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
           -- It is safe now to create the default style file in @dir@ without overwriting
           -- a possibly user-edited copy there.
           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 a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
             styFile <- [Char] -> IO [Char]
    getDataFileName ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $
               [Char]
    latexDataDir [Char] -> ShowS
    </> [Char]
    defaultStyFile
             copyFile styFile agdaSty

    -- | 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 (Interface -> TopLevelModuleName
    iTopLevelModuleName Interface
    i)
      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 RangeFile -> Text -> HighlightingInfo -> m Text
    forall (m :: * -> *).
    MonadLogLaTeX m =>
    Env -> Maybe RangeFile -> Text -> HighlightingInfo -> m Text
    toLaTeX
                  (TextWidthEstimator -> Env
    emptyEnv TextWidthEstimator
    textWidthEstimator)
                  (LaTeXOptions -> Maybe RangeFile
    latexOptSourceFileName LaTeXOptions
    opts)
                  (Interface -> Text
    iSource Interface
    i)
                  (Interface -> HighlightingInfo
    iHighlighting Interface
    i)
      liftIO $ do
        createDirectoryIfMissing True (takeDirectory outPath)
        BS.writeFile outPath latex

    latexOutRelativeFilePath :: TopLevelModuleName -> FilePath
    latexOutRelativeFilePath :: TopLevelModuleName -> [Char]
    latexOutRelativeFilePath TopLevelModuleName
    m =
      [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char
    pathSeparator]
        ((Text -> [Char]) -> [Text] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> [Char]
    T.unpack ([Text] -> [[Char]]) -> [Text] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleNameParts -> [Item TopLevelModuleNameParts]
    forall l. IsList l => l -> [Item l]
    List1.toList (TopLevelModuleNameParts -> [Item TopLevelModuleNameParts])
    -> TopLevelModuleNameParts -> [Item TopLevelModuleNameParts]
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> TopLevelModuleNameParts
    forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
    moduleNameParts TopLevelModuleName
    m) [Char] -> ShowS
    <.>
      [Char]
    "tex"

    -- | Transforms the source code into LaTeX.
    toLaTeX
      :: MonadLogLaTeX m
      => Env
      -> Maybe RangeFile
      -> L.Text
      -> HighlightingInfo
      -> m L.Text
    toLaTeX :: forall (m :: * -> *).
    MonadLogLaTeX m =>
    Env -> Maybe RangeFile -> Text -> HighlightingInfo -> m Text
    toLaTeX Env
    env Maybe RangeFile
    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, List1 (Maybe Aspects, Char)) -> (LayerRole, [Token]))
    -> [(LayerRole, List1 (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 b a. IsBool b => b -> (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, List1 (Maybe Aspects, Char))
        -> (LayerRole, [Token]))
    -> (LayerRole, List1 (Maybe Aspects, Char))
    -> (LayerRole, [Token])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ( (List1 (Maybe Aspects, Char) -> [Token])
    -> (LayerRole, List1 (Maybe Aspects, Char)) -> (LayerRole, [Token])
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    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])
    -> (List1 (Maybe Aspects, Char) -> [Token])
    -> List1 (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])
    -> (List1 (Maybe Aspects, Char) -> [Token])
    -> List1 (Maybe Aspects, Char)
    -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty Token -> [Item (NonEmpty Token)]
    NonEmpty Token -> [Token]
    forall l. IsList l => l -> [Item l]
    List1.toList
                    (NonEmpty Token -> [Token])
    -> (List1 (Maybe Aspects, Char) -> NonEmpty Token)
    -> List1 (Maybe Aspects, Char)
    -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Maybe Aspects, List1 Char) -> Token)
    -> NonEmpty (Maybe Aspects, List1 Char) -> NonEmpty Token
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ (Maybe Aspects
    mi, List1 Char
    cs) -> Token
                            { text :: Text
    text = [Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ List1 Char -> [Item (List1 Char)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 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
                            }
                          )
                    (NonEmpty (Maybe Aspects, List1 Char) -> NonEmpty Token)
    -> (List1 (Maybe Aspects, Char)
        -> NonEmpty (Maybe Aspects, List1 Char))
    -> List1 (Maybe Aspects, Char)
    -> NonEmpty Token
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (Maybe Aspects, Char) -> NonEmpty (Maybe Aspects, List1 Char)
    forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
    List1.groupByFst1
                    )
                )
          )
        ([(LayerRole, List1 (Maybe Aspects, Char))]
     -> [(LayerRole, [Token])])
    -> ([Char] -> [(LayerRole, List1 (Maybe Aspects, Char))])
    -> [Char]
    -> [(LayerRole, [Token])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(LayerRole, (Maybe Aspects, Char))]
    -> [(LayerRole, List1 (Maybe Aspects, Char))]
    forall a b. Eq a => [(a, b)] -> [(a, List1 b)]
    List1.groupByFst

        -- Look up the meta info at each position in the highlighting info.
        ([(LayerRole, (Maybe Aspects, Char))]
     -> [(LayerRole, List1 (Maybe Aspects, Char))])
    -> ([Char] -> [(LayerRole, (Maybe Aspects, Char))])
    -> [Char]
    -> [(LayerRole, List1 (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..]
        -- Map each character to its role
        ([(LayerRole, Char)] -> [(LayerRole, (Maybe Aspects, Char))])
    -> ([Char] -> [(LayerRole, Char)])
    -> [Char]
    -> [(LayerRole, (Maybe Aspects, Char))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Layers -> [(LayerRole, Char)]
    atomizeLayers
        (Layers -> [(LayerRole, Char)])
    -> ([Char] -> Layers) -> [Char] -> [(LayerRole, Char)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Processor
    literateTeX (() -> Position' ()
    forall a. a -> Position' a
    startPos' ())
        ([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
      ((), s, os) <- LaTeXT m () -> Env -> State -> m ((), State, [Output])
    forall (m :: * -> *) a.
    MonadLogLaTeX m =>
    LaTeXT m a -> Env -> State -> m (a, State, [Output])
    runLaTeX ([(LayerRole, [Token])] -> LaTeXT m ()
    forall (m :: * -> *).
    MonadLogLaTeX m =>
    [(LayerRole, [Token])] -> LaTeXT m ()
    processLayers [(LayerRole, [Token])]
    ts) Env
    env State
    emptyState
      return $ L.fromChunks $ map (render s) 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