{-# 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 -> LaTeXT m () -> LaTeXT 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 -> LaTeXT m ()
forall (m :: * -> *). MonadLogLaTeX m => Int -> LaTeXT m ()
moveColumn (Int -> LaTeXT m ())
-> RWST Env [Output] State m Int -> LaTeXT 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
  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 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
                   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 = succ nextId }
                   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 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
nextId)
  let c :: AlignmentColumn
c = 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 = c : columns s }
  AlignmentColumn -> LaTeXT m AlignmentColumn
forall a. a -> RWST Env [Output] State m a
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 = Set.insert i (usedColumns 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 -> LaTeXT m AlignmentColumn
forall a. a -> RWST Env [Output] State m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AlignmentColumn -> LaTeXT m AlignmentColumn)
-> AlignmentColumn -> LaTeXT m AlignmentColumn
forall a b. (a -> b) -> a -> b
$ 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 <- LaTeXT m AlignmentColumn
LaTeX AlignmentColumn
columnZero
  (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 { 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
  [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 -> LaTeXT m () -> LaTeXT m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Debug
debug Debug -> [Debug] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Debug]
logLevels) (LaTeXT m () -> LaTeXT m ()) -> LaTeXT m () -> LaTeXT m ()
forall a b. (a -> b) -> a -> b
$ do
    m () -> LaTeXT m ()
forall (m :: * -> *) a.
Monad m =>
m a -> RWST Env [Output] State m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> LaTeXT m ()) -> m () -> LaTeXT 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 :: 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.
      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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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] -> LaTeX ()
spaces ([Text] -> LaTeX ()) -> [Text] -> LaTeX ()
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 ()
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
$
            -- 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 a b. (a -> b -> b) -> b -> [a] -> b
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 a. Set a -> [a]
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 a. Maybe a -> [a]
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 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
  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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Int
col Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) do
    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
  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
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 -> RWST Env [Output] State m ()
forall (m :: * -> *). MonadLogLaTeX m => Int -> LaTeXT m ()
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 -> LaTeX ()) -> Text -> LaTeX ()
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 ()
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 -> 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
$ 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 = 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.
  Bool
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
  Bool -> m () -> m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless Bool
dirExisted (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    -- Create directory @dir@ and parent directories.
    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
$ Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True [Char]
dir

  -- Check whether TeX will find @agda.sty@.
  Either IOException [Char]
texFindsSty <- IO (Either IOException [Char]) -> m (Either IOException [Char])
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either IOException [Char]) -> m (Either IOException [Char]))
-> IO (Either IOException [Char]) -> m (Either IOException [Char])
forall a b. (a -> b) -> a -> b
$ IO [Char] -> IO (Either IOException [Char])
forall e a. Exception e => IO a -> IO (Either e a)
try (IO [Char] -> IO (Either IOException [Char]))
-> IO [Char] -> IO (Either IOException [Char])
forall a b. (a -> b) -> a -> b
$
      [Char] -> [[Char]] -> [Char] -> IO [Char]
readProcess
        [Char]
"kpsewhich"
        (Bool -> ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
dirExisted (([Char]
"--path=" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
dir) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:) [[Char]
defaultStyFile])
        [Char]
""
  case Either IOException [Char]
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
         [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]
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)
  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 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)
  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
    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]
    ((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
  ((), State
s, [Output]
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
  Text -> m Text
forall a. a -> m a
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