module Agda.TypeChecking.Monad.Trace where

import Prelude hiding (null)

import Control.Monad.Reader

import qualified Data.Set as Set

import Agda.Syntax.Position
import qualified Agda.Syntax.Position as P

import Agda.Interaction.Response
import Agda.Interaction.Highlighting.Precise
import Agda.Interaction.Highlighting.Range (rToR, minus)

import Agda.TypeChecking.Monad.Base
  hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State

import Agda.Utils.Function

import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)

---------------------------------------------------------------------------
-- * Trace
---------------------------------------------------------------------------

interestingCall :: Call -> Bool
interestingCall :: Call -> Bool
interestingCall = \case
    InferVar{}              -> Bool
False
    InferDef{}              -> Bool
False
    CheckArguments Range
_ [] Type
_ Maybe Type
_ -> Bool
False
    SetRange{}              -> Bool
False
    NoHighlighting{}        -> Bool
False
    -- Andreas, 2019-08-07, expanded catch-all pattern.
    -- The previous presence of a catch-all raises the following question:
    -- are all of the following really interesting?
    CheckClause{}             -> Bool
True
    CheckLHS{}                -> Bool
True
    CheckPattern{}            -> Bool
True
    CheckLetBinding{}         -> Bool
True
    InferExpr{}               -> Bool
True
    CheckExprCall{}           -> Bool
True
    CheckDotPattern{}         -> Bool
True
    IsTypeCall{}              -> Bool
True
    IsType_{}                 -> Bool
True
    CheckArguments{}          -> Bool
True
    CheckMetaSolution{}       -> Bool
True
    CheckTargetType{}         -> Bool
True
    CheckDataDef{}            -> Bool
True
    CheckRecDef{}             -> Bool
True
    CheckConstructor{}        -> Bool
True
    CheckConstructorFitsIn{}  -> Bool
True
    CheckFunDefCall{}         -> Bool
True
    CheckPragma{}             -> Bool
True
    CheckPrimitive{}          -> Bool
True
    CheckIsEmpty{}            -> Bool
True
    CheckConfluence{}         -> Bool
True
    CheckWithFunctionType{}   -> Bool
True
    CheckSectionApplication{} -> Bool
True
    CheckNamedWhere{}         -> Bool
True
    ScopeCheckExpr{}          -> Bool
True
    ScopeCheckDeclaration{}   -> Bool
True
    ScopeCheckLHS{}           -> Bool
True
    CheckProjection{}         -> Bool
True
    ModuleContents{}          -> Bool
True

traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a
traceCallM :: tcm Call -> tcm a -> tcm a
traceCallM tcm Call
call tcm a
m = (Call -> tcm a -> tcm a) -> tcm a -> Call -> tcm a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Call -> tcm a -> tcm a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall tcm a
m (Call -> tcm a) -> tcm Call -> tcm a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< tcm Call
call

-- | Reset 'envCall' to previous value in the continuation.
--
-- Caveat: if the last 'traceCall' did not set an 'interestingCall',
-- for example, only set the 'Range' with 'SetRange',
-- we will revert to the last interesting call.

traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm)
  => Call
  -> ((a -> tcm b) -> tcm b)
  -> ((a -> tcm b) -> tcm b)
traceCallCPS :: Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b
traceCallCPS Call
call (a -> tcm b) -> tcm b
k a -> tcm b
ret = do
  Maybe (Closure Call)
mcall <- (TCEnv -> Maybe (Closure Call)) -> tcm (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
  Call -> tcm b -> tcm b
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall Call
call (tcm b -> tcm b) -> tcm b -> tcm b
forall a b. (a -> b) -> a -> b
$ (a -> tcm b) -> tcm b
k ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b
forall a b. (a -> b) -> a -> b
$ \ a
a -> do
    (tcm b -> tcm b)
-> (Closure Call -> tcm b -> tcm b)
-> Maybe (Closure Call)
-> tcm b
-> tcm b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe tcm b -> tcm b
forall a. a -> a
id Closure Call -> tcm b -> tcm b
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Closure Call -> tcm a -> tcm a
traceClosureCall Maybe (Closure Call)
mcall (tcm b -> tcm b) -> tcm b -> tcm b
forall a b. (a -> b) -> a -> b
$ a -> tcm b
ret a
a

-- | Record a function call in the trace.

-- RULE left-hand side too complicated to desugar
-- {-# SPECIALIZE traceCall :: Call -> TCM a -> TCM a #-}
traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a
traceCall :: Call -> tcm a -> tcm a
traceCall Call
call tcm a
m = do
  Closure Call
cl <- TCM (Closure Call) -> tcm (Closure Call)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Closure Call) -> tcm (Closure Call))
-> TCM (Closure Call) -> tcm (Closure Call)
forall a b. (a -> b) -> a -> b
$ Call -> TCM (Closure Call)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Call
call
  Closure Call -> tcm a -> tcm a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Closure Call -> tcm a -> tcm a
traceClosureCall Closure Call
cl tcm a
m

traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a
traceClosureCall :: Closure Call -> tcm a -> tcm a
traceClosureCall Closure Call
cl tcm a
m = do

  -- Andreas, 2016-09-13 issue #2177
  -- Since the fix of #2092 we may report an error outside the current file.
  -- (For instance, if we import a module which then happens to have the
  -- wrong name.)
  -- Thus, we no longer crash, but just report the alien range.
  -- -- Andreas, 2015-02-09 Make sure we do not set a range
  -- -- outside the current file
  VerboseKey -> VerboseLevel -> tcm () -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"check.ranges" VerboseLevel
90 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$
    Maybe AbsolutePath -> (AbsolutePath -> tcm ()) -> tcm ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
Strict.whenJust (Range -> Maybe AbsolutePath
rangeFile Range
callRange) ((AbsolutePath -> tcm ()) -> tcm ())
-> (AbsolutePath -> tcm ()) -> tcm ()
forall a b. (a -> b) -> a -> b
$ \AbsolutePath
f -> do
      Maybe AbsolutePath
currentFile <- (TCEnv -> Maybe AbsolutePath) -> tcm (Maybe AbsolutePath)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe AbsolutePath
envCurrentPath
      Bool -> tcm () -> tcm ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe AbsolutePath
currentFile Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
/= AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just AbsolutePath
f) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ do
        VerboseKey -> VerboseLevel -> VerboseKey -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"check.ranges" VerboseLevel
90 (VerboseKey -> tcm ()) -> VerboseKey -> tcm ()
forall a b. (a -> b) -> a -> b
$
          Call -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Call
call VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
          VerboseKey
" is setting the current range to " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Range -> VerboseKey
forall a. Show a => a -> VerboseKey
show Range
callRange VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
          VerboseKey
" which is outside of the current file " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Maybe AbsolutePath -> VerboseKey
forall a. Show a => a -> VerboseKey
show Maybe AbsolutePath
currentFile

  -- Compute update to 'Range' and 'Call' components of 'TCEnv'.
  let withCall :: tcm a -> tcm a
withCall = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ ((TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv)
-> (TCEnv -> TCEnv) -> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) TCEnv -> TCEnv
forall a. a -> a
id ([TCEnv -> TCEnv] -> TCEnv -> TCEnv)
-> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
forall a b. (a -> b) -> a -> b
$ [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv])
-> [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
forall a b. (a -> b) -> a -> b
$
        [ [ \TCEnv
e -> TCEnv
e { envCall :: Maybe (Closure Call)
envCall = Closure Call -> Maybe (Closure Call)
forall a. a -> Maybe a
Just Closure Call
cl } | Call -> Bool
interestingCall Call
call ]
        , [ \TCEnv
e -> TCEnv
e { envHighlightingRange :: Range
envHighlightingRange = Range
callRange }
          | Bool
callHasRange Bool -> Bool -> Bool
&& Bool
highlightCall
            Bool -> Bool -> Bool
|| Bool
isNoHighlighting
          ]
        , [ \TCEnv
e -> TCEnv
e { envRange :: Range
envRange = Range
callRange } | Bool
callHasRange ]
        ]

  -- For interactive highlighting, also wrap computation @m@ in 'highlightAsTypeChecked':
  tcm Bool -> tcm a -> tcm a -> tcm a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (Bool -> tcm Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
highlightCall tcm Bool -> tcm Bool -> tcm Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do (HighlightingLevel
Interactive HighlightingLevel -> HighlightingLevel -> Bool
forall a. Eq a => a -> a -> Bool
==) (HighlightingLevel -> Bool)
-> (TCEnv -> HighlightingLevel) -> TCEnv -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> HighlightingLevel
envHighlightingLevel (TCEnv -> Bool) -> tcm TCEnv -> tcm Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tcm TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC)
    {-then-} (tcm a -> tcm a
forall a. tcm a -> tcm a
withCall tcm a
m)
    {-else-} (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ do
      Range
oldRange <- TCEnv -> Range
envHighlightingRange (TCEnv -> Range) -> tcm TCEnv -> tcm Range
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tcm TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
      Range -> Range -> tcm a -> tcm a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm) =>
Range -> Range -> tcm a -> tcm a
highlightAsTypeChecked Range
oldRange Range
callRange (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$
        tcm a -> tcm a
forall a. tcm a -> tcm a
withCall tcm a
m
  where
  call :: Call
call = Closure Call -> Call
forall a. Closure a -> a
clValue Closure Call
cl
  callRange :: Range
callRange = Call -> Range
forall t. HasRange t => t -> Range
getRange Call
call
  callHasRange :: Bool
callHasRange = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Range -> Bool
forall a. Null a => a -> Bool
null Range
callRange

  -- | Should the given call trigger interactive highlighting?
  highlightCall :: Bool
highlightCall = case Call
call of
    CheckClause{}             -> Bool
True
    CheckLHS{}                -> Bool
True
    CheckPattern{}            -> Bool
True
    CheckLetBinding{}         -> Bool
True
    InferExpr{}               -> Bool
True
    CheckExprCall{}           -> Bool
True
    CheckDotPattern{}         -> Bool
True
    IsTypeCall{}              -> Bool
True
    IsType_{}                 -> Bool
True
    InferVar{}                -> Bool
True
    InferDef{}                -> Bool
True
    CheckArguments{}          -> Bool
True
    CheckMetaSolution{}       -> Bool
False
    CheckTargetType{}         -> Bool
False
    CheckDataDef{}            -> Bool
True
    CheckRecDef{}             -> Bool
True
    CheckConstructor{}        -> Bool
True
    CheckConstructorFitsIn{}  -> Bool
False
    CheckFunDefCall{}         -> Bool
True
    CheckPragma{}             -> Bool
True
    CheckPrimitive{}          -> Bool
True
    CheckIsEmpty{}            -> Bool
True
    CheckConfluence{}         -> Bool
False
    CheckWithFunctionType{}   -> Bool
True
    CheckSectionApplication{} -> Bool
True
    CheckNamedWhere{}         -> Bool
False
    ScopeCheckExpr{}          -> Bool
False
    ScopeCheckDeclaration{}   -> Bool
False
    ScopeCheckLHS{}           -> Bool
False
    NoHighlighting{}          -> Bool
True
    CheckProjection{}         -> Bool
False
    SetRange{}                -> Bool
False
    ModuleContents{}          -> Bool
False

  isNoHighlighting :: Bool
isNoHighlighting = case Call
call of
    NoHighlighting{} -> Bool
True
    Call
_ -> Bool
False

getCurrentRange :: MonadTCEnv m => m Range
getCurrentRange :: m Range
getCurrentRange = (TCEnv -> Range) -> m Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange

-- | Sets the current range (for error messages etc.) to the range
--   of the given object, if it has a range (i.e., its range is not 'noRange').
setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x)
                => x -> tcm a -> tcm a
setCurrentRange :: x -> tcm a -> tcm a
setCurrentRange x
x = Bool -> (tcm a -> tcm a) -> tcm a -> tcm a
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Range -> Bool
forall a. Null a => a -> Bool
null Range
r) ((tcm a -> tcm a) -> tcm a -> tcm a)
-> (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Call -> tcm a -> tcm a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Call -> tcm a -> tcm a) -> Call -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Range -> Call
SetRange Range
r
  where r :: Range
r = x -> Range
forall t. HasRange t => t -> Range
getRange x
x

-- | @highlightAsTypeChecked rPre r m@ runs @m@ and returns its
--   result. Additionally, some code may be highlighted:
--
-- * If @r@ is non-empty and not a sub-range of @rPre@ (after
--   'P.continuousPerLine' has been applied to both): @r@ is
--   highlighted as being type-checked while @m@ is running (this
--   highlighting is removed if @m@ completes /successfully/).
--
-- * Otherwise: Highlighting is removed for @rPre - r@ before @m@
--   runs, and if @m@ completes successfully, then @rPre - r@ is
--   highlighted as being type-checked.

highlightAsTypeChecked
  :: (MonadTCM tcm, ReadTCState tcm)
  => Range   -- ^ @rPre@
  -> Range   -- ^ @r@
  -> tcm a
  -> tcm a
highlightAsTypeChecked :: Range -> Range -> tcm a -> tcm a
highlightAsTypeChecked Range
rPre Range
r tcm a
m
  | Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= Range
forall a. Range' a
noRange Bool -> Bool -> Bool
&& Ranges
delta Ranges -> Ranges -> Bool
forall a. Eq a => a -> a -> Bool
== Ranges
rPre' = Ranges -> Aspects -> Aspects -> tcm a
wrap Ranges
r'    Aspects
highlight Aspects
clear
  | Bool
otherwise                      = Ranges -> Aspects -> Aspects -> tcm a
wrap Ranges
delta Aspects
clear     Aspects
highlight
  where
  rPre' :: Ranges
rPre'     = Range -> Ranges
rToR (Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
rPre)
  r' :: Ranges
r'        = Range -> Ranges
rToR (Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r)
  delta :: Ranges
delta     = Ranges
rPre' Ranges -> Ranges -> Ranges
`minus` Ranges
r'
  clear :: Aspects
clear     = Aspects
forall a. Monoid a => a
mempty
  highlight :: Aspects
highlight = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
TypeChecks }

  wrap :: Ranges -> Aspects -> Aspects -> tcm a
wrap Ranges
rs Aspects
x Aspects
y = do
    Ranges -> Aspects -> tcm ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
Ranges -> Aspects -> tcm ()
p Ranges
rs Aspects
x
    a
v <- tcm a
m
    Ranges -> Aspects -> tcm ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
Ranges -> Aspects -> tcm ()
p Ranges
rs Aspects
y
    a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v
    where
    p :: Ranges -> Aspects -> tcm ()
p Ranges
rs Aspects
x = RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Ranges -> Aspects -> HighlightingInfo
singletonC Ranges
rs Aspects
x)

-- | Lispify and print the given highlighting information.

printHighlightingInfo ::
  (MonadTCM tcm, ReadTCState tcm) =>
  RemoveTokenBasedHighlighting ->
  HighlightingInfo ->
  tcm ()
printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
remove HighlightingInfo
info = do
  Map TopLevelModuleName AbsolutePath
modToSrc <- Lens' (Map TopLevelModuleName AbsolutePath) TCState
-> tcm (Map TopLevelModuleName AbsolutePath)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
stModuleToSource
  HighlightingMethod
method   <- Lens' HighlightingMethod TCEnv -> tcm HighlightingMethod
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' HighlightingMethod TCEnv
eHighlightingMethod
  TCM () -> tcm ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> tcm ()) -> TCM () -> tcm ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> [VerboseKey] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"highlighting" VerboseLevel
50
    [ VerboseKey
"Printing highlighting info:"
    , HighlightingInfo -> VerboseKey
forall a. Show a => a -> VerboseKey
show HighlightingInfo
info
    , VerboseKey
"  modToSrc = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Map TopLevelModuleName AbsolutePath -> VerboseKey
forall a. Show a => a -> VerboseKey
show Map TopLevelModuleName AbsolutePath
modToSrc
    ]
  Bool -> tcm () -> tcm ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Range, Aspects)] -> Bool
forall a. Null a => a -> Bool
null ([(Range, Aspects)] -> Bool) -> [(Range, Aspects)] -> Bool
forall a b. (a -> b) -> a -> b
$ HighlightingInfo -> [(Range, Aspects)]
ranges HighlightingInfo
info) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ do
    TCM () -> tcm ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> tcm ()) -> TCM () -> tcm ()
forall a b. (a -> b) -> a -> b
$ Response -> TCM ()
appInteractionOutputCallback (Response -> TCM ()) -> Response -> TCM ()
forall a b. (a -> b) -> a -> b
$
        HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> Map TopLevelModuleName AbsolutePath
-> Response
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method Map TopLevelModuleName AbsolutePath
modToSrc