Agda.TypeChecking.Monad.Trace

Trace

interestingCall :: Call -> Bool

traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a

traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b

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 Call, we will revert to the last interesting call.

traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a

Record a function call in the trace.

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

getCurrentRange :: MonadTCEnv m => m Range

setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a

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

highlightAsTypeChecked

Arguments

:: (MonadTCM tcm, ReadTCState tcm)

=> Range

rPre

-> Range

r

-> tcm a

-> tcm a

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

printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()

Lispify and print the given highlighting information.