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

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

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

import Prelude hiding (log)

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

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

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

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

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

import Paths_Agda

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

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

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

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

import Agda.Utils.Impossible

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

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

-- | Log LaTeX messages using a provided action.
--
-- This could be accomplished by putting logs into the RWST output and splitting it
-- into a WriterT, but that becomes slightly more complicated to reason about in
-- the presence of IO exceptions.
--
-- We want the logging to be reasonably polymorphic, avoid space leaks that can occur
-- with WriterT, and also be usable during outer phases such as directory preparation.
--
-- I'm not certain this is the best way to do it, but whatever.
type LogLaTeXT m = ReaderT (LogMessage -> m ()) m

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

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

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

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

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

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

-- | Output items.

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

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

-- | Column kinds.

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

-- | Unique identifiers for indentation columns.

type IndentationColumnId = Int

-- | Alignment and indentation columns.

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

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

type TextWidthEstimator = Text -> Int

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

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

type Tokens = [Token]

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

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

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

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

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

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


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

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

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

-- | Does the string consist solely of whitespace?

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

-- | Registers column zero as an alignment column.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Opens a column with the given name.

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

-- | Opens the given column.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    Debug -> Text -> LaTeX ()
log Debug
Spaces (Text -> 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 -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ Text
ptOpenBeginningOfLine
        Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
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 -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Int -> Text
ptOpenIndent AlignmentColumn
c (Int
codeBlock Int -> Int -> Int
forall a. Num a => a -> a -> a
- AlignmentColumn -> Int
columnCodeBlock AlignmentColumn
c)
      [AlignmentColumn]
_ -> () -> RWST Env [Output] State m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Output
MaybeColumn AlignmentColumn
column

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

stringLiteral Token
t = [Token
t]

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

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

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

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

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

data LaTeXOptions = LaTeXOptions
  { LaTeXOptions -> [Char]
latexOptOutDir         :: FilePath
  , LaTeXOptions -> Maybe AbsolutePath
latexOptSourceFileName :: Maybe AbsolutePath
    -- ^ The parser uses a @Position@ which includes a source filename for
    -- error reporting and such. We don't actually get the source filename
    -- with an @Interface@, and it isn't necessary to look it up.
    -- This is a "nice-to-have" parameter.
  , LaTeXOptions -> Bool
latexOptCountClusters  :: Bool
    -- ^ Count extended grapheme clusters rather than code points when
    -- generating LaTeX.
  }

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

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

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

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

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

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

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

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

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

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

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

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


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