    -- | Generates data used for precise syntax highlighting.

    -- {-# OPTIONS_GHC -fwarn-unused-imports #-}  -- Semigroup import obsolete in later ghcs
    -- {-# OPTIONS_GHC -fwarn-unused-binds   #-}

    module Agda.Interaction.Highlighting.Generate
      ( Level(..)
      , generateAndPrintSyntaxInfo
      , generateTokenInfo, generateTokenInfoFromSource
      , generateTokenInfoFromString
      , printSyntaxInfo
      , printErrorInfo, errorHighlighting
      , printUnsolvedInfo
      , printHighlightingInfo
      , highlightAsTypeChecked
      , highlightWarning, warningHighlighting
      , computeUnsolvedInfo
      , storeDisambiguatedConstructor, storeDisambiguatedProjection
      , disambiguateRecordFields
      ) where

    import Prelude hiding (null)

    import Control.Monad
    import Control.Arrow (second)

    import qualified Data.Foldable as Fold
    import qualified Data.Map as Map
    import Data.Maybe
    import Data.List ((\\))
    import qualified Data.List as List
    import qualified Data.IntMap as IntMap
    import Data.HashMap.Strict (HashMap)
    import qualified Data.HashMap.Strict as HMap
    import Data.Semigroup (Semigroup(..))
    import Data.Sequence (Seq)
    import qualified Data.Set as Set
    import qualified Data.Text.Lazy as Text

    import Agda.Interaction.Response
      ( RemoveTokenBasedHighlighting( KeepHighlighting ) )
    import Agda.Interaction.Highlighting.Precise as H
    import Agda.Interaction.Highlighting.Range
      (rToR, rangeToRange, overlappings, Ranges)
    import Agda.Interaction.Highlighting.FromAbstract

    import qualified Agda.TypeChecking.Errors as TCM
    import Agda.TypeChecking.MetaVars (isBlockedTerm, hasTwinMeta)
    import Agda.TypeChecking.Monad
      hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
    import qualified Agda.TypeChecking.Monad  as TCM
    import qualified Agda.TypeChecking.Pretty as TCM
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Warnings ( raiseWarningsOnUsage, runPM )

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..), DeclarationWarning'(..) )
    import Agda.Syntax.Common (pattern Ranged)
    import qualified Agda.Syntax.Common as Common
    import qualified Agda.Syntax.Concrete.Name as C
    import qualified Agda.Syntax.Internal as I
    import qualified Agda.Syntax.Literal as L
    import qualified Agda.Syntax.Parser as Pa
    import qualified Agda.Syntax.Parser.Tokens as T
    import qualified Agda.Syntax.Position as P
    import Agda.Syntax.Position (Range, HasRange, getRange, noRange)

    import Agda.Syntax.Scope.Base     ( WithKind(..) )
    import Agda.Syntax.Abstract.Views ( KName, declaredNames )

    import Agda.Utils.FileName
    import Agda.Utils.List            ( caseList, initWithDefault, last1 )
    import Agda.Utils.List2           ( List2 )
    import qualified Agda.Utils.List2 as List2
    import Agda.Utils.Maybe
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Null
    import Agda.Utils.Pretty
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    -- | Highlighting levels.

    data Level
      = Full
        -- ^ Full highlighting. Should only be used after typechecking has
        --   completed successfully.
      | Partial
        -- ^ Highlighting without disambiguation of overloaded
        --   constructors.

    -- | Highlight a warning.
    --   We do not generate highlighting for unsolved metas and
    --   constraints, as that gets handled in bulk after typechecking.
    highlightWarning :: TCWarning -> TCM ()
    highlightWarning :: TCWarning -> TCM ()
    highlightWarning TCWarning
    tcwarn = do
      let h :: HighlightingInfo
    h = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' Bool
    False TCWarning
    tcwarn
      -- Highlighting for warnings coming from the Happy parser is placed
      -- together with token highlighting.
      case TCWarning -> Warning
    tcWarning TCWarning
    tcwarn of
        ParseWarning{} -> Lens' HighlightingInfo TCState
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' HighlightingInfo TCState
    stTokens     (HighlightingInfo
    h HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>)
        Warning
    _              -> Lens' HighlightingInfo TCState
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' HighlightingInfo TCState
    stSyntaxInfo (HighlightingInfo
    h HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>)
      HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingInfo
    h

    -- | Generate syntax highlighting information for the given
    -- declaration, and (if appropriate) print it. If the boolean is
    -- 'True', then the state is additionally updated with the new
    -- highlighting info (in case of a conflict new info takes precedence
    -- over old info).
    --
    -- The procedure makes use of some of the highlighting info
    -- corresponding to 'stTokens' (that corresponding to the interval
    -- covered by the declaration). If the boolean is 'True', then this
    -- highlighting info is additionally removed from the data structure
    -- that 'stTokens' refers to.

    generateAndPrintSyntaxInfo
      :: A.Declaration
           -- ^ Declaration to highlight.
      -> Level
           -- ^ Amount of highlighting.
      -> Bool
           -- ^ Update the state?
      -> TCM ()
    generateAndPrintSyntaxInfo :: Declaration -> Level -> Bool -> TCM ()
    generateAndPrintSyntaxInfo Declaration
    decl Level
    _ Bool
    _ | Range -> Bool
    forall a. Null a => a -> Bool
    null (Range -> Bool) -> Range -> Bool
    forall a b. (a -> b) -> a -> b
    $ Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    decl = () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    generateAndPrintSyntaxInfo Declaration
    decl Level
    hlLevel Bool
    updateState = do
      AbsolutePath
    file <- TCMT IO AbsolutePath
    forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
    getCurrentPath

      [Char] -> Key -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Key -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Key
    15 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
        [ [Char]
    "Generating syntax info for "
        , AbsolutePath -> [Char]
    filePath AbsolutePath
    file
        , case Level
    hlLevel of
            Full   {} -> [Char]
    " (final)."
            Partial{} -> [Char]
    " (first approximation)."
        ]

      TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        SourceToModule
    modMap <- TCM SourceToModule
    sourceToModule
        NameKinds
    kinds  <- Level -> Declaration -> TCM NameKinds
    nameKinds Level
    hlLevel Declaration
    decl

        -- After the code has been type checked more information may be
        -- available for overloaded constructors, and
        -- @generateConstructorInfo@ takes advantage of this information.
        -- Note, however, that highlighting for overloaded constructors is
        -- included also in @nameInfo@.
        HighlightingInfoBuilder
    constructorInfo <- case Level
    hlLevel of
          Full{} -> SourceToModule
    -> AbsolutePath
    -> NameKinds
    -> Declaration
    -> TCMT IO HighlightingInfoBuilder
    generateConstructorInfo SourceToModule
    modMap AbsolutePath
    file NameKinds
    kinds Declaration
    decl
          Level
    _      -> HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty

        -- Main source of scope-checker generated highlighting:
        let nameInfo :: HighlightingInfoBuilder
    nameInfo = SourceToModule
    -> AbsolutePath
    -> NameKinds
    -> Declaration
    -> HighlightingInfoBuilder
    forall a.
    Hilite a =>
    SourceToModule
    -> AbsolutePath -> NameKinds -> a -> HighlightingInfoBuilder
    runHighlighter SourceToModule
    modMap AbsolutePath
    file NameKinds
    kinds Declaration
    decl

        [Char] -> Key -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Key -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "highlighting.warning" Key
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCM.hcat
          [ TCMT IO Doc
    "current path = "
          , TCMT IO Doc
    -> (AbsolutePath -> TCMT IO Doc) -> SrcFile -> TCMT IO Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    Strict.maybe TCMT IO Doc
    "(nothing)" (Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc)
    -> (AbsolutePath -> Doc) -> AbsolutePath -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> Doc
    forall a. Pretty a => a -> Doc
    pretty) (SrcFile -> TCMT IO Doc) -> TCMT IO SrcFile -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              Range -> SrcFile
    P.rangeFile (Range -> SrcFile) -> TCMT IO Range -> TCMT IO SrcFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' Range TCEnv -> TCMT IO Range
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' Range TCEnv
    eRange
          ]

        -- Highlighting from the lexer and Happy parser:
        (HighlightingInfo
    curTokens, HighlightingInfo
    otherTokens) <-
          Range -> HighlightingInfo -> (HighlightingInfo, HighlightingInfo)
    forall a. Range -> RangeMap a -> (RangeMap a, RangeMap a)
    insideAndOutside (Range -> Range
    rangeToRange (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    decl)) (HighlightingInfo -> (HighlightingInfo, HighlightingInfo))
    -> TCMT IO HighlightingInfo
    -> TCMT IO (HighlightingInfo, HighlightingInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' HighlightingInfo TCState
    stTokens

        -- @constructorInfo@ needs
        -- to be placed before @nameInfo@ since, when typechecking is done,
        -- constructors are included in both lists. Finally the token
        -- information is placed last since token highlighting is more
        -- crude than the others.
        let syntaxInfo :: HighlightingInfo
    syntaxInfo = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder
    constructorInfo HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Semigroup a => a -> a -> a
    <> HighlightingInfoBuilder
    nameInfo)
                           HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>
                         HighlightingInfo
    curTokens

        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    updateState (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Lens' HighlightingInfo TCState
    stSyntaxInfo Lens' HighlightingInfo TCState
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Monoid a => a -> a -> a
    mappend HighlightingInfo
    syntaxInfo
          Lens' HighlightingInfo TCState
    stTokens     Lens' HighlightingInfo TCState -> HighlightingInfo -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens`    HighlightingInfo
    otherTokens

        HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingInfo
    syntaxInfo

    -- | Generate and return the syntax highlighting information for the
    -- tokens in the given file.

    generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo
    generateTokenInfo :: AbsolutePath -> TCMT IO HighlightingInfo
    generateTokenInfo AbsolutePath
    file =
      AbsolutePath -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromSource AbsolutePath
    file ([Char] -> TCMT IO HighlightingInfo)
    -> (Text -> [Char]) -> Text -> TCMT IO HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> [Char]
    Text.unpack (Text -> TCMT IO HighlightingInfo)
    -> TCMT IO Text -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
        PM Text -> TCMT IO Text
    forall a. PM a -> TCM a
    runPM (AbsolutePath -> PM Text
    Pa.readFilePM AbsolutePath
    file)

    -- | Generate and return the syntax highlighting information for the
    -- tokens in the given file.

    generateTokenInfoFromSource
      :: AbsolutePath
         -- ^ The module to highlight.
      -> String
         -- ^ The file contents. Note that the file is /not/ read from
         -- disk.
      -> TCM HighlightingInfo
    generateTokenInfoFromSource :: AbsolutePath -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromSource AbsolutePath
    file [Char]
    input =
      PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a. PM a -> TCM a
    runPM (PM HighlightingInfo -> TCMT IO HighlightingInfo)
    -> PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ [Token] -> HighlightingInfo
    tokenHighlighting ([Token] -> HighlightingInfo)
    -> (([Token], FileType) -> [Token])
    -> ([Token], FileType)
    -> HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Token], FileType) -> [Token]
    forall a b. (a, b) -> a
    fst (([Token], FileType) -> HighlightingInfo)
    -> PM ([Token], FileType) -> PM HighlightingInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser [Token] -> AbsolutePath -> [Char] -> PM ([Token], FileType)
    forall a.
    Show a =>
    Parser a -> AbsolutePath -> [Char] -> PM (a, FileType)
    Pa.parseFile Parser [Token]
    Pa.tokensParser AbsolutePath
    file [Char]
    input

    -- | Generate and return the syntax highlighting information for the
    -- tokens in the given string, which is assumed to correspond to the
    -- given range.

    generateTokenInfoFromString :: Range -> String -> TCM HighlightingInfo
    generateTokenInfoFromString :: Range -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromString Range
    r [Char]
    _ | Range
    r Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    forall a. Range' a
    noRange = HighlightingInfo -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingInfo
    forall a. Monoid a => a
    mempty
    generateTokenInfoFromString Range
    r [Char]
    s = do
      PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a. PM a -> TCM a
    runPM (PM HighlightingInfo -> TCMT IO HighlightingInfo)
    -> PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ [Token] -> HighlightingInfo
    tokenHighlighting ([Token] -> HighlightingInfo) -> PM [Token] -> PM HighlightingInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser [Token] -> Position -> [Char] -> PM [Token]
    forall a. Parser a -> Position -> [Char] -> PM a
    Pa.parsePosString Parser [Token]
    Pa.tokensParser Position
    p [Char]
    s
      where
        Just Position
    p = Range -> Maybe Position
    forall a. Range' a -> Maybe (Position' a)
    P.rStart Range
    r

    -- | Compute syntax highlighting for the given tokens.
    tokenHighlighting :: [T.Token] -> HighlightingInfo
    tokenHighlighting :: [Token] -> HighlightingInfo
    tokenHighlighting = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> ([Token] -> HighlightingInfoBuilder)
    -> [Token]
    -> HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [HighlightingInfoBuilder] -> HighlightingInfoBuilder
    forall a. Monoid a => [a] -> a
    mconcat ([HighlightingInfoBuilder] -> HighlightingInfoBuilder)
    -> ([Token] -> [HighlightingInfoBuilder])
    -> [Token]
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Token -> HighlightingInfoBuilder)
    -> [Token] -> [HighlightingInfoBuilder]
    forall a b. (a -> b) -> [a] -> [b]
    map Token -> HighlightingInfoBuilder
    tokenToHI
      where
      -- Converts an aspect and a range to a file.
      aToF :: Aspect -> Range -> m
    aToF Aspect
    a Range
    r = Ranges -> Aspects -> m
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR Range
    r) (Aspects
    forall a. Monoid a => a
    mempty { aspect :: Maybe Aspect
    aspect = Aspect -> Maybe Aspect
    forall a. a -> Maybe a
    Just Aspect
    a })

      tokenToHI :: T.Token -> HighlightingInfoBuilder
      tokenToHI :: Token -> HighlightingInfoBuilder
    tokenToHI (T.TokKeyword Keyword
    T.KwForall Interval
    i)  = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Symbol (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokKeyword Keyword
    T.KwREWRITE Interval
    _) = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty  -- #4361, REWRITE is not always a Keyword
      tokenToHI (T.TokKeyword Keyword
    _ Interval
    i)           = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Keyword (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokSymbol Symbol
    T.SymQuestionMark Interval
    i) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Hole (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokSymbol  Symbol
    _ Interval
    i)                = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Symbol (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitNat    Integer
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Number Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitWord64 Word64
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Number Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitFloat  Double
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Number Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitString Text
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitChar   Char
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitQName  QName
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitMeta AbsolutePath
    _ MetaId
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokComment (Interval
    i, [Char]
    _))            = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Comment (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokTeX (Interval
    i, [Char]
    _))                = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Background (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokMarkup (Interval
    i, [Char]
    _))             = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Markup (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokId {})                     = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      tokenToHI (T.TokQId {})                    = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      tokenToHI (T.TokString (Interval
    i,[Char]
    s))              = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Pragma (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokDummy {})                  = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      tokenToHI (T.TokEOF {})                    = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty

    -- | Builds a 'NameKinds' function.

    nameKinds :: Level
                 -- ^ This should only be @'Full'@ if
                 -- type-checking completed successfully (without any
                 -- errors).
              -> A.Declaration
              -> TCM NameKinds
    nameKinds :: Level -> Declaration -> TCM NameKinds
    nameKinds Level
    hlLevel Declaration
    decl = do
      HashMap QName Definition
    imported <- Lens' (HashMap QName Definition) TCState
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC (Lens' (HashMap QName Definition) TCState
     -> TCMT IO (HashMap QName Definition))
    -> Lens' (HashMap QName Definition) TCState
    -> TCMT IO (HashMap QName Definition)
    forall a b. (a -> b) -> a -> b
    $ (Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stImports ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' (HashMap QName Definition) Signature
    sigDefinitions
      HashMap QName Definition
    local    <- case Level
    hlLevel of
        Full{} -> Lens' (HashMap QName Definition) TCState
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC (Lens' (HashMap QName Definition) TCState
     -> TCMT IO (HashMap QName Definition))
    -> Lens' (HashMap QName Definition) TCState
    -> TCMT IO (HashMap QName Definition)
    forall a b. (a -> b) -> a -> b
    $ (Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stSignature ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' (HashMap QName Definition) Signature
    sigDefinitions
        Level
    _      -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. Monad m => a -> m a
    return HashMap QName Definition
    forall k v. HashMap k v
    HMap.empty
      Map QName PatternSynDefn
    impPatSyns <- Lens' (Map QName PatternSynDefn) TCState
    -> TCMT IO (Map QName PatternSynDefn)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map QName PatternSynDefn) TCState
    stPatternSynImports
      Map QName PatternSynDefn
    locPatSyns <- case Level
    hlLevel of
        Full{} -> Lens' (Map QName PatternSynDefn) TCState
    -> TCMT IO (Map QName PatternSynDefn)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map QName PatternSynDefn) TCState
    stPatternSyns
        Level
    _      -> Map QName PatternSynDefn -> TCMT IO (Map QName PatternSynDefn)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map QName PatternSynDefn
    forall a. Null a => a
    empty
          -- Traverses the syntax tree and constructs a map from qualified
          -- names to name kinds. TODO: Handle open public.
      let syntax :: NameKindMap
          syntax :: NameKindMap
    syntax = NameKindBuilder -> NameKindMap -> NameKindMap
    runBuilder (Declaration -> NameKindBuilder
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames Declaration
    decl :: NameKindBuilder) NameKindMap
    forall k v. HashMap k v
    HMap.empty
      NameKinds -> TCM NameKinds
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NameKinds -> TCM NameKinds) -> NameKinds -> TCM NameKinds
    forall a b. (a -> b) -> a -> b
    $ \ QName
    n -> (NameKind -> NameKind -> NameKind)
    -> [Maybe NameKind] -> Maybe NameKind
    forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
    unionsMaybeWith NameKind -> NameKind -> NameKind
    mergeNameKind
        [ Defn -> NameKind
    defnToKind (Defn -> NameKind)
    -> (Definition -> Defn) -> Definition -> NameKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> HashMap QName Definition -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    n HashMap QName Definition
    local
        , NameKind
    con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    n Map QName PatternSynDefn
    locPatSyns
        , Defn -> NameKind
    defnToKind (Defn -> NameKind)
    -> (Definition -> Defn) -> Definition -> NameKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> HashMap QName Definition -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    n HashMap QName Definition
    imported
        , NameKind
    con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    n Map QName PatternSynDefn
    impPatSyns
        , QName -> NameKindMap -> Maybe NameKind
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    n NameKindMap
    syntax
        ]
      where
      defnToKind :: TCM.Defn -> NameKind
      defnToKind :: Defn -> NameKind
    defnToKind   TCM.Axiom{}                           = NameKind
    Postulate
      defnToKind   TCM.DataOrRecSig{}                    = NameKind
    Postulate
      defnToKind   TCM.GeneralizableVar{}                = NameKind
    Generalizable
      defnToKind d :: Defn
    d@TCM.Function{} | Defn -> Bool
    isProperProjection Defn
    d = NameKind
    Field
                                | Bool
    otherwise            = NameKind
    Function
      defnToKind   TCM.Datatype{}                        = NameKind
    Datatype
      defnToKind   TCM.Record{}                          = NameKind
    Record
      defnToKind   TCM.Constructor{ conInd :: Defn -> Induction
    TCM.conInd = Induction
    i }       = Induction -> NameKind
    Constructor Induction
    i
      defnToKind   TCM.Primitive{}                       = NameKind
    Primitive
      defnToKind   TCM.PrimitiveSort{}                   = NameKind
    Primitive
      defnToKind   TCM.AbstractDefn{}                    = NameKind
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      con :: NameKind
      con :: NameKind
    con = Induction -> NameKind
    Constructor Induction
    Common.Inductive

    -- | The 'TCM.Axiom' constructor is used to represent various things
    -- which are not really axioms, so when maps are merged 'Postulate's
    -- are thrown away whenever possible. The 'declaredNames' function
    -- below can return several explanations for one qualified name; the
    -- 'Postulate's are bogus.
    mergeNameKind :: NameKind -> NameKind -> NameKind
    mergeNameKind :: NameKind -> NameKind -> NameKind
    mergeNameKind NameKind
    Postulate NameKind
    k = NameKind
    k
    mergeNameKind NameKind
    _     NameKind
    Macro = NameKind
    Macro  -- If the abstract syntax says macro, it's a macro.
    mergeNameKind NameKind
    k         NameKind
    _ = NameKind
    k

    -- Auxiliary types for @nameKinds@ generation

    type NameKindMap     = HashMap A.QName NameKind
    data NameKindBuilder = NameKindBuilder
      { NameKindBuilder -> NameKindMap -> NameKindMap
    runBuilder :: NameKindMap -> NameKindMap
      }

    instance Semigroup (NameKindBuilder) where
      NameKindBuilder NameKindMap -> NameKindMap
    f <> :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
    <> NameKindBuilder NameKindMap -> NameKindMap
    g = (NameKindMap -> NameKindMap) -> NameKindBuilder
    NameKindBuilder ((NameKindMap -> NameKindMap) -> NameKindBuilder)
    -> (NameKindMap -> NameKindMap) -> NameKindBuilder
    forall a b. (a -> b) -> a -> b
    $ NameKindMap -> NameKindMap
    f (NameKindMap -> NameKindMap)
    -> (NameKindMap -> NameKindMap) -> NameKindMap -> NameKindMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NameKindMap -> NameKindMap
    g

    instance Monoid (NameKindBuilder) where
      mempty :: NameKindBuilder
    mempty = (NameKindMap -> NameKindMap) -> NameKindBuilder
    NameKindBuilder NameKindMap -> NameKindMap
    forall a. a -> a
    id
      mappend :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
    mappend = NameKindBuilder -> NameKindBuilder -> NameKindBuilder
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance Singleton KName NameKindBuilder where
      singleton :: KName -> NameKindBuilder
    singleton (WithKind KindOfName
    k QName
    q) = (NameKindMap -> NameKindMap) -> NameKindBuilder
    NameKindBuilder ((NameKindMap -> NameKindMap) -> NameKindBuilder)
    -> (NameKindMap -> NameKindMap) -> NameKindBuilder
    forall a b. (a -> b) -> a -> b
    $
        (NameKind -> NameKind -> NameKind)
    -> QName -> NameKind -> NameKindMap -> NameKindMap
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
    HMap.insertWith NameKind -> NameKind -> NameKind
    mergeNameKind QName
    q (NameKind -> NameKindMap -> NameKindMap)
    -> NameKind -> NameKindMap -> NameKindMap
    forall a b. (a -> b) -> a -> b
    $ KindOfName -> NameKind
    kindOfNameToNameKind KindOfName
    k

    instance Collection KName NameKindBuilder

    -- | Generates syntax highlighting information for all constructors
    -- occurring in patterns and expressions in the given declaration.
    --
    -- This function should only be called after type checking.
    -- Constructors can be overloaded, and the overloading is resolved by
    -- the type checker.

    generateConstructorInfo
      :: SourceToModule  -- ^ Maps source file paths to module names.
      -> AbsolutePath    -- ^ The module to highlight.
      -> NameKinds
      -> A.Declaration
      -> TCM HighlightingInfoBuilder
    generateConstructorInfo :: SourceToModule
    -> AbsolutePath
    -> NameKinds
    -> Declaration
    -> TCMT IO HighlightingInfoBuilder
    generateConstructorInfo SourceToModule
    modMap AbsolutePath
    file NameKinds
    kinds Declaration
    decl = do

      -- Get boundaries of current declaration.
      -- @noRange@ should be impossible, but in case of @noRange@
      -- it makes sense to return mempty.
      [IntervalWithoutFile]
    -> TCMT IO HighlightingInfoBuilder
    -> (IntervalWithoutFile
        -> [IntervalWithoutFile] -> TCMT IO HighlightingInfoBuilder)
    -> TCMT IO HighlightingInfoBuilder
    forall a b. [a] -> b -> (a -> [a] -> b) -> b
    caseList (Range -> [IntervalWithoutFile]
    forall a. Range' a -> [IntervalWithoutFile]
    P.rangeIntervals (Range -> [IntervalWithoutFile]) -> Range -> [IntervalWithoutFile]
    forall a b. (a -> b) -> a -> b
    $ Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    decl)
               (HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty) ((IntervalWithoutFile
      -> [IntervalWithoutFile] -> TCMT IO HighlightingInfoBuilder)
     -> TCMT IO HighlightingInfoBuilder)
    -> (IntervalWithoutFile
        -> [IntervalWithoutFile] -> TCMT IO HighlightingInfoBuilder)
    -> TCMT IO HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ \ IntervalWithoutFile
    i [IntervalWithoutFile]
    is -> do
        let start :: Key
    start = Int32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int32 -> Key) -> Int32 -> Key
    forall a b. (a -> b) -> a -> b
    $ Position' () -> Int32
    forall a. Position' a -> Int32
    P.posPos (Position' () -> Int32) -> Position' () -> Int32
    forall a b. (a -> b) -> a -> b
    $ IntervalWithoutFile -> Position' ()
    forall a. Interval' a -> Position' a
    P.iStart IntervalWithoutFile
    i
            end :: Key
    end   = Int32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int32 -> Key) -> Int32 -> Key
    forall a b. (a -> b) -> a -> b
    $ Position' () -> Int32
    forall a. Position' a -> Int32
    P.posPos (Position' () -> Int32) -> Position' () -> Int32
    forall a b. (a -> b) -> a -> b
    $ IntervalWithoutFile -> Position' ()
    forall a. Interval' a -> Position' a
    P.iEnd (IntervalWithoutFile -> Position' ())
    -> IntervalWithoutFile -> Position' ()
    forall a b. (a -> b) -> a -> b
    $ IntervalWithoutFile -> [IntervalWithoutFile] -> IntervalWithoutFile
    forall a. a -> [a] -> a
    last1 IntervalWithoutFile
    i [IntervalWithoutFile]
    is

        -- Get all disambiguated names that fall within the range of decl.
        IntMap DisambiguatedName
    m0 <- Lens' (IntMap DisambiguatedName) TCState
    -> TCMT IO (IntMap DisambiguatedName)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (IntMap DisambiguatedName) TCState
    stDisambiguatedNames
        let (IntMap DisambiguatedName
    _, IntMap DisambiguatedName
    m1) = Key
    -> IntMap DisambiguatedName
    -> (IntMap DisambiguatedName, IntMap DisambiguatedName)
    forall a. Key -> IntMap a -> (IntMap a, IntMap a)
    IntMap.split (Key -> Key
    forall a. Enum a => a -> a
    pred Key
    start) IntMap DisambiguatedName
    m0
            (IntMap DisambiguatedName
    m2, IntMap DisambiguatedName
    _) = Key
    -> IntMap DisambiguatedName
    -> (IntMap DisambiguatedName, IntMap DisambiguatedName)
    forall a. Key -> IntMap a -> (IntMap a, IntMap a)
    IntMap.split Key
    end IntMap DisambiguatedName
    m1
            constrs :: [DisambiguatedName]
    constrs = IntMap DisambiguatedName -> [DisambiguatedName]
    forall a. IntMap a -> [a]
    IntMap.elems IntMap DisambiguatedName
    m2

        -- Return suitable syntax highlighting information.
        HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder)
    -> HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ (DisambiguatedName -> HighlightingInfoBuilder)
    -> [DisambiguatedName] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (SourceToModule
    -> AbsolutePath
    -> NameKinds
    -> DisambiguatedName
    -> HighlightingInfoBuilder
    forall a.
    Hilite a =>
    SourceToModule
    -> AbsolutePath -> NameKinds -> a -> HighlightingInfoBuilder
    runHighlighter SourceToModule
    modMap AbsolutePath
    file NameKinds
    kinds) [DisambiguatedName]
    constrs

    printSyntaxInfo :: Range -> TCM ()
    printSyntaxInfo :: Range -> TCM ()
    printSyntaxInfo Range
    r = do
      HighlightingInfo
    syntaxInfo <- Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' HighlightingInfo TCState
    stSyntaxInfo
      HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting
          (Range -> HighlightingInfo -> HighlightingInfo
    forall a. Range -> RangeMap a -> RangeMap a
    restrictTo (Range -> Range
    rangeToRange Range
    r) HighlightingInfo
    syntaxInfo)

    -- | Prints syntax highlighting info for an error.

    printErrorInfo :: TCErr -> TCM ()
    printErrorInfo :: TCErr -> TCM ()
    printErrorInfo TCErr
    e =
      RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (HighlightingInfo -> TCM ())
    -> (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> TCM ())
    -> TCMT IO HighlightingInfoBuilder -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
        TCErr -> TCMT IO HighlightingInfoBuilder
    errorHighlighting TCErr
    e

    -- | Generate highlighting for error.

    errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
    errorHighlighting :: TCErr -> TCMT IO HighlightingInfoBuilder
    errorHighlighting TCErr
    e = Range -> [Char] -> HighlightingInfoBuilder
    errorHighlighting' (TCErr -> Range
    forall a. HasRange a => a -> Range
    getRange TCErr
    e) ([Char] -> HighlightingInfoBuilder)
    -> TCMT IO [Char] -> TCMT IO HighlightingInfoBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCErr -> TCMT IO [Char]
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
    TCM.prettyError TCErr
    e

    errorHighlighting'
      :: Range     -- ^ Error range.
      -> String    -- ^ Error message for tooltip.
      -> HighlightingInfoBuilder
    errorHighlighting' :: Range -> [Char] -> HighlightingInfoBuilder
    errorHighlighting' Range
    r [Char]
    s = [HighlightingInfoBuilder] -> HighlightingInfoBuilder
    forall a. Monoid a => [a] -> a
    mconcat
      [ -- Erase previous highlighting.
        Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    forall a. Monoid a => a
    mempty
      , -- Print new highlighting.
        Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR Range
    r)
             (Aspects -> HighlightingInfoBuilder)
    -> Aspects -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    Error
                           , note :: [Char]
    note         = [Char]
    s
                           }
      ]

    -- | Highlighting for warnings that are considered fatal.

    errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting a
    w =
      Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    w) (Aspects -> HighlightingInfoBuilder)
    -> Aspects -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
        Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    ErrorWarning }
    -- errorWarningHighlighting w = errorHighlighting' (getRange w) ""
      -- MonadPretty not available here, so, no tooltip.
      -- errorHighlighting' (getRange w) . render <$> TCM.prettyWarning (tcWarning w)

    -- | Generate syntax highlighting for warnings.

    warningHighlighting :: TCWarning -> HighlightingInfoBuilder
    warningHighlighting :: TCWarning -> HighlightingInfoBuilder
    warningHighlighting = Bool -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' Bool
    True

    warningHighlighting' :: Bool -- ^ should we generate highlighting for unsolved metas and constrains?
                         -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' :: Bool -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' Bool
    b TCWarning
    w = case TCWarning -> Warning
    tcWarning TCWarning
    w of
      TerminationIssue [TerminationError]
    terrs     -> [TerminationError] -> HighlightingInfoBuilder
    terminationErrorHighlighting [TerminationError]
    terrs
      NotStrictlyPositive QName
    d Seq OccursWhere
    ocs  -> QName -> Seq OccursWhere -> HighlightingInfoBuilder
    positivityErrorHighlighting QName
    d Seq OccursWhere
    ocs
      -- #3965 highlight each unreachable clause independently: they
      -- may be interleaved with actually reachable clauses!
      UnreachableClauses QName
    _ [Range]
    rs    -> (Range -> HighlightingInfoBuilder)
    -> [Range] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting [Range]
    rs
      CoverageIssue{}            -> Range -> HighlightingInfoBuilder
    coverageErrorHighlighting (Range -> HighlightingInfoBuilder)
    -> Range -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> Range
    forall a. HasRange a => a -> Range
    getRange TCWarning
    w
      CoverageNoExactSplit{}     -> Range -> HighlightingInfoBuilder
    catchallHighlighting (Range -> HighlightingInfoBuilder)
    -> Range -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> Range
    forall a. HasRange a => a -> Range
    getRange TCWarning
    w
      UnsolvedConstraints Constraints
    cs     -> if Bool
    b then [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting [] Constraints
    cs else HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UnsolvedMetaVariables [Range]
    rs   -> if Bool
    b then [Range] -> HighlightingInfoBuilder
    metasHighlighting [Range]
    rs          else HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      AbsurdPatternRequiresNoRHS{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      ModuleDoesntExport{}         -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      DuplicateUsing List1 ImportedName
    xs            -> (ImportedName -> HighlightingInfoBuilder)
    -> List1 ImportedName -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ImportedName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 ImportedName
    xs
      FixityInRenamingModule List1 Range
    rs    -> (Range -> HighlightingInfoBuilder)
    -> List1 Range -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 Range
    rs
      -- expanded catch-all case to get a warning for new constructors
      CantGeneralizeOverSorts{}  -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UnsolvedInteractionMetas{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      OldBuiltin{}               -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      EmptyRewritePragma{}       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      EmptyWhere{}               -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      IllformedAsClause{}        -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UselessPublic{}            -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UselessHiding [ImportedName]
    xs           -> (ImportedName -> HighlightingInfoBuilder)
    -> [ImportedName] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ImportedName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting [ImportedName]
    xs
      UselessInline{}            -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UselessPatternDeclarationForRecord{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      ClashesViaRenaming NameOrModule
    _ [Name]
    xs    -> (Name -> HighlightingInfoBuilder)
    -> [Name] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Name -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting [Name]
    xs
        -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
        -- Should we have a different color?
      WrongInstanceDeclaration{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      InstanceWithExplicitArg{}  -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      InstanceNoOutputTypeName{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      InstanceArgWithExplicitArg{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      InversionDepthReached{}    -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      NoGuardednessFlag{}        -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      GenericWarning{}           -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      GenericUseless Range
    r Doc
    _         -> Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting Range
    r
      -- Andreas, 2020-03-21, issue #4456:
      -- Error warnings that do not have dedicated highlighting
      -- are highlighted as errors.
      GenericNonFatalError{}                -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      SafeFlagPostulate{}                   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      SafeFlagPragma{}                      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagNonTerminating                -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagTerminating                   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagWithoutKFlagPrimEraseEquality -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagEta                           -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagInjective                     -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagNoCoverageCheck               -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagNoPositivityCheck             -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagPolarity                      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagNoUniverseCheck               -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      InfectiveImport{}                     -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      CoInfectiveImport{}                   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    WithoutKFlagPrimEraseEquality -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      DeprecationWarning{}       -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UserWarning{}              -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      LibraryWarning{}           -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      RewriteNonConfluent{}      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      RewriteMaybeNonConfluent{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      RewriteAmbiguousRules{}    -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      RewriteMissingRule{}       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      PragmaCompileErased{}      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      NotInScopeW{}              -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      AsPatternShadowsConstructorOrPatternSynonym{}
                                 -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      RecordFieldWarning RecordFieldWarning
    w       -> RecordFieldWarning -> HighlightingInfoBuilder
    recordFieldWarningHighlighting RecordFieldWarning
    w
      ParseWarning ParseWarning
    w             -> case ParseWarning
    w of
        Pa.UnsupportedAttribute{}     -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.MultipleAttributes{}       -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.OverlappingTokensWarning{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      NicifierIssue (DeclarationWarning CallStack
    _ DeclarationWarning'
    w) -> case DeclarationWarning'
    w of
        -- we intentionally override the binding of `w` here so that our pattern of
        -- using `getRange w` still yields the most precise range information we
        -- can get.
        NotAllowedInMutual{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyAbstract{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyConstructor{}               -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyInstance{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyMacro{}                     -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyMutual{}                    -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPostulate{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPrimitive{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPrivate{}                   -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyGeneralize{}                -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyField{}                     -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        UselessAbstract{}                -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        UselessInstance{}                -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        UselessPrivate{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidNoPositivityCheckPragma{} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidNoUniverseCheckPragma{}   -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidTerminationCheckPragma{}  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidCoverageCheckPragma{}     -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidConstructor{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidConstructorBlock{}        -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidRecordDirective{}         -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        OpenPublicAbstract{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        OpenPublicPrivate{}              -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        W.ShadowingInTelescope List1 (Name, List2 Range)
    nrs       -> ((Name, List2 Range) -> HighlightingInfoBuilder)
    -> List1 (Name, List2 Range) -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap
                                              (List2 Range -> HighlightingInfoBuilder
    shadowingTelHighlighting (List2 Range -> HighlightingInfoBuilder)
    -> ((Name, List2 Range) -> List2 Range)
    -> (Name, List2 Range)
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, List2 Range) -> List2 Range
    forall a b. (a, b) -> b
    snd)
                                              List1 (Name, List2 Range)
    nrs
        MissingDeclarations{}            -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting DeclarationWarning'
    w
        MissingDefinitions{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting DeclarationWarning'
    w
        -- TODO: explore highlighting opportunities here!
        InvalidCatchallPragma{}           -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        PolarityPragmasButNotPostulates{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        PragmaNoTerminationCheck{}        -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        PragmaCompiled{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        UnknownFixityInMixfixDecl{}       -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        UnknownNamesInFixityDecl{}        -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        UnknownNamesInPolarityPragmas{}   -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty

    recordFieldWarningHighlighting ::
      RecordFieldWarning -> HighlightingInfoBuilder
    recordFieldWarningHighlighting :: RecordFieldWarning -> HighlightingInfoBuilder
    recordFieldWarningHighlighting = \case
      DuplicateFieldsWarning [(Name, Range)]
    xrs      -> [(Name, Range)] -> HighlightingInfoBuilder
    dead [(Name, Range)]
    xrs
      TooManyFieldsWarning QName
    _q [Name]
    _ys [(Name, Range)]
    xrs -> [(Name, Range)] -> HighlightingInfoBuilder
    dead [(Name, Range)]
    xrs
      where
      dead :: [(C.Name, Range)] -> HighlightingInfoBuilder
      dead :: [(Name, Range)] -> HighlightingInfoBuilder
    dead = [HighlightingInfoBuilder] -> HighlightingInfoBuilder
    forall a. Monoid a => [a] -> a
    mconcat ([HighlightingInfoBuilder] -> HighlightingInfoBuilder)
    -> ([(Name, Range)] -> [HighlightingInfoBuilder])
    -> [(Name, Range)]
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Name, Range) -> HighlightingInfoBuilder)
    -> [(Name, Range)] -> [HighlightingInfoBuilder]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Range) -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting
      -- Andreas, 2020-03-27 #3684: This variant seems to only highlight @x@:
      -- dead = mconcat . map f
      -- f (x, r) = deadcodeHighlighting (getRange x) `mappend` deadcodeHighlighting r

    -- | Generate syntax highlighting for termination errors.

    terminationErrorHighlighting ::
      [TerminationError] -> HighlightingInfoBuilder
    terminationErrorHighlighting :: [TerminationError] -> HighlightingInfoBuilder
    terminationErrorHighlighting [TerminationError]
    termErrs = HighlightingInfoBuilder
    functionDefs HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Monoid a => a -> a -> a
    `mappend` HighlightingInfoBuilder
    callSites
      where
        m :: Aspects
    m            = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    TerminationProblem }
        functionDefs :: HighlightingInfoBuilder
    functionDefs = (QName -> HighlightingInfoBuilder)
    -> [QName] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (\QName
    x -> Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    bindingSite QName
    x) Aspects
    m) ([QName] -> HighlightingInfoBuilder)
    -> [QName] -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
                       (TerminationError -> [QName]) -> [TerminationError] -> [QName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap TerminationError -> [QName]
    termErrFunctions [TerminationError]
    termErrs
        callSites :: HighlightingInfoBuilder
    callSites    = (Range -> HighlightingInfoBuilder)
    -> [Range] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (\Range
    r -> Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR Range
    r) Aspects
    m) ([Range] -> HighlightingInfoBuilder)
    -> [Range] -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
                       (TerminationError -> [Range]) -> [TerminationError] -> [Range]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((CallInfo -> Range) -> [CallInfo] -> [Range]
    forall a b. (a -> b) -> [a] -> [b]
    map CallInfo -> Range
    callInfoRange ([CallInfo] -> [Range])
    -> (TerminationError -> [CallInfo]) -> TerminationError -> [Range]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TerminationError -> [CallInfo]
    termErrCalls) [TerminationError]
    termErrs
        bindingSite :: QName -> Range
    bindingSite  = Name -> Range
    A.nameBindingSite (Name -> Range) -> (QName -> Name) -> QName -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName

    -- | Generate syntax highlighting for not-strictly-positive inductive
    -- definitions.

    positivityErrorHighlighting ::
      I.QName -> Seq OccursWhere -> HighlightingInfoBuilder
    positivityErrorHighlighting :: QName -> Seq OccursWhere -> HighlightingInfoBuilder
    positivityErrorHighlighting QName
    q Seq OccursWhere
    os =
      [Ranges] -> Aspects -> HighlightingInfoBuilder
    forall a hl.
    (IsBasicRangeMap a hl, Monoid hl) =>
    [Ranges] -> a -> hl
    several (Range -> Ranges
    rToR (Range -> Ranges) -> [Range] -> [Ranges]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    q Range -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    : [Range]
    rs) Aspects
    m
      where
        rs :: [Range]
    rs = (OccursWhere -> Range) -> [OccursWhere] -> [Range]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(OccursWhere Range
    r Seq Where
    _ Seq Where
    _) -> Range
    r) (Seq OccursWhere -> [OccursWhere]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList Seq OccursWhere
    os)
        m :: Aspects
    m  = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    PositivityProblem }

    deadcodeHighlighting :: HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Range' a -> Range' a
    P.continuous (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    Deadcode }

    coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
    coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
    coverageErrorHighlighting Range
    r = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    CoverageProblem }

    shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
    shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
    shadowingTelHighlighting =
      -- we do not want to highlight the one variable in scope so we take
      -- the @init@ segment of the ranges in question
      (Range -> HighlightingInfoBuilder)
    -> List1 Range -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (\Range
    r -> Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Range' a -> Range' a
    P.continuous Range
    r) Aspects
    m) (List1 Range -> HighlightingInfoBuilder)
    -> (List2 Range -> List1 Range)
    -> List2 Range
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List2 Range -> List1 Range
    forall a. List2 a -> List1 a
    List2.init
      where
      m :: Aspects
    m = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects =
                          OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    H.ShadowingInTelescope }

    catchallHighlighting :: Range -> HighlightingInfoBuilder
    catchallHighlighting :: Range -> HighlightingInfoBuilder
    catchallHighlighting Range
    r = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    CatchallClause }

    confluenceErrorHighlighting ::
      HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    ConfluenceProblem }

    missingDefinitionHighlighting ::
      HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    MissingDefinition }

    -- | Generates and prints syntax highlighting information for unsolved
    -- meta-variables and certain unsolved constraints.

    printUnsolvedInfo :: TCM ()
    printUnsolvedInfo :: TCM ()
    printUnsolvedInfo = do
      HighlightingInfoBuilder
    info <- TCMT IO HighlightingInfoBuilder
    computeUnsolvedInfo

      RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert HighlightingInfoBuilder
    info)

    computeUnsolvedInfo :: TCM HighlightingInfoBuilder
    computeUnsolvedInfo :: TCMT IO HighlightingInfoBuilder
    computeUnsolvedInfo = do
      ([Ranges]
    rs, HighlightingInfoBuilder
    metaInfo) <- TCM ([Ranges], HighlightingInfoBuilder)
    computeUnsolvedMetaWarnings
      HighlightingInfoBuilder
    constraintInfo <- [Ranges] -> TCMT IO HighlightingInfoBuilder
    computeUnsolvedConstraints [Ranges]
    rs

      HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder)
    -> HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ HighlightingInfoBuilder
    metaInfo HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Monoid a => a -> a -> a
    `mappend` HighlightingInfoBuilder
    constraintInfo

    -- | Generates syntax highlighting information for unsolved meta
    -- variables.
    --   Also returns ranges of unsolved or interaction metas.
    computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
    computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
    computeUnsolvedMetaWarnings = do
      [MetaId]
    is <- TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getInteractionMetas

      -- We don't want to highlight blocked terms, since
      --   * there is always at least one proper meta responsible for the blocking
      --   * in many cases the blocked term covers the highlighting for this meta
      --   * for the same reason we skip metas with a twin, since the twin will be blocked.
      let notBlocked :: MetaId -> TCMT IO Bool
    notBlocked MetaId
    m = Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Bool
    isBlockedTerm MetaId
    m
      let notHasTwin :: MetaId -> TCMT IO Bool
    notHasTwin MetaId
    m = Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Bool
    hasTwinMeta MetaId
    m
      [MetaId]
    ms <- (MetaId -> TCMT IO Bool) -> [MetaId] -> TCMT IO [MetaId]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM MetaId -> TCMT IO Bool
    notHasTwin ([MetaId] -> TCMT IO [MetaId])
    -> TCMT IO [MetaId] -> TCMT IO [MetaId]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (MetaId -> TCMT IO Bool) -> [MetaId] -> TCMT IO [MetaId]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM MetaId -> TCMT IO Bool
    notBlocked ([MetaId] -> TCMT IO [MetaId])
    -> TCMT IO [MetaId] -> TCMT IO [MetaId]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas

      let extend :: [Range] -> [Ranges]
    extend = (Range -> Ranges) -> [Range] -> [Ranges]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range -> Ranges
    rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine)

      [Ranges]
    rs <- [Range] -> [Ranges]
    extend ([Range] -> [Ranges]) -> TCMT IO [Range] -> TCMT IO [Ranges]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (MetaId -> TCMT IO Range) -> [MetaId] -> TCMT IO [Range]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange ([MetaId]
    ms [MetaId] -> [MetaId] -> [MetaId]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ [MetaId]
    is)

      [Ranges]
    rs' <- [Range] -> [Ranges]
    extend ([Range] -> [Ranges]) -> TCMT IO [Range] -> TCMT IO [Ranges]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (MetaId -> TCMT IO Range) -> [MetaId] -> TCMT IO [Range]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange [MetaId]
    is
      ([Ranges], HighlightingInfoBuilder)
    -> TCM ([Ranges], HighlightingInfoBuilder)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Ranges], HighlightingInfoBuilder)
     -> TCM ([Ranges], HighlightingInfoBuilder))
    -> ([Ranges], HighlightingInfoBuilder)
    -> TCM ([Ranges], HighlightingInfoBuilder)
    forall a b. (a -> b) -> a -> b
    $ ([Ranges]
    rs [Ranges] -> [Ranges] -> [Ranges]
    forall a. [a] -> [a] -> [a]
    ++ [Ranges]
    rs', [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' [Ranges]
    rs)

    metasHighlighting :: [Range] -> HighlightingInfoBuilder
    metasHighlighting :: [Range] -> HighlightingInfoBuilder
    metasHighlighting [Range]
    rs = [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' ((Range -> Ranges) -> [Range] -> [Ranges]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range -> Ranges
    rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine) [Range]
    rs)

    metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' [Ranges]
    rs = [Ranges] -> Aspects -> HighlightingInfoBuilder
    forall a hl.
    (IsBasicRangeMap a hl, Monoid hl) =>
    [Ranges] -> a -> hl
    several [Ranges]
    rs
                         (Aspects -> HighlightingInfoBuilder)
    -> Aspects -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    UnsolvedMeta }

    -- | Generates syntax highlighting information for unsolved constraints
    --   (ideally: that are not connected to a meta variable).

    computeUnsolvedConstraints :: [Ranges] -- ^ does not add ranges that would overlap with these.
                               -> TCM HighlightingInfoBuilder
    computeUnsolvedConstraints :: [Ranges] -> TCMT IO HighlightingInfoBuilder
    computeUnsolvedConstraints [Ranges]
    ms = [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting [Ranges]
    ms (Constraints -> HighlightingInfoBuilder)
    -> TCMT IO Constraints -> TCMT IO HighlightingInfoBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    getAllConstraints

    constraintsHighlighting ::
      [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting :: [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting [Ranges]
    ms Constraints
    cs =
      [Ranges] -> Aspects -> HighlightingInfoBuilder
    forall a hl.
    (IsBasicRangeMap a hl, Monoid hl) =>
    [Ranges] -> a -> hl
    several ((Ranges -> Bool) -> [Ranges] -> [Ranges]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Ranges -> Bool
    noOverlap ([Ranges] -> [Ranges]) -> [Ranges] -> [Ranges]
    forall a b. (a -> b) -> a -> b
    $ (Range -> Ranges) -> [Range] -> [Ranges]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range -> Ranges
    rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine) [Range]
    rs)
              (Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    UnsolvedConstraint })
      where
      noOverlap :: Ranges -> Bool
    noOverlap Ranges
    r = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Ranges -> Bool) -> [Ranges] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Ranges -> Ranges -> Bool
    overlappings (Ranges -> Ranges -> Bool) -> Ranges -> Ranges -> Bool
    forall a b. (a -> b) -> a -> b
    $ Ranges
    r) ([Ranges] -> Bool) -> [Ranges] -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Ranges]
    ms
      -- get ranges of interesting unsolved constraints
      rs :: [Range]
    rs = ((Closure Constraint -> Maybe Range)
    -> [Closure Constraint] -> [Range]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    `mapMaybe` ((ProblemConstraint -> Closure Constraint)
    -> Constraints -> [Closure Constraint]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> Closure Constraint
    theConstraint Constraints
    cs)) ((Closure Constraint -> Maybe Range) -> [Range])
    -> (Closure Constraint -> Maybe Range) -> [Range]
    forall a b. (a -> b) -> a -> b
    $ \case
        Closure{ clValue :: forall a. Closure a -> a
    clValue = IsEmpty Range
    r Type
    t           } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just Range
    r
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = ValueCmp{} } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = ElimCmp{}  } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = SortCmp{}  } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = LevelCmp{} } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = CheckSizeLtSat{} } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure Constraint
    _ -> Maybe Range
    forall a. Maybe a
    Nothing

    -- * Disambiguation of constructors and projections.

    storeDisambiguatedField :: A.QName -> TCM ()
    storeDisambiguatedField :: QName -> TCM ()
    storeDisambiguatedField = NameKind -> QName -> TCM ()
    storeDisambiguatedName NameKind
    Field

    storeDisambiguatedProjection :: A.QName -> TCM ()
    storeDisambiguatedProjection :: QName -> TCM ()
    storeDisambiguatedProjection = QName -> TCM ()
    storeDisambiguatedField

    storeDisambiguatedConstructor :: Common.Induction -> A.QName -> TCM ()
    storeDisambiguatedConstructor :: Induction -> QName -> TCM ()
    storeDisambiguatedConstructor Induction
    i = NameKind -> QName -> TCM ()
    storeDisambiguatedName (NameKind -> QName -> TCM ()) -> NameKind -> QName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Induction -> NameKind
    Constructor Induction
    i

    -- TODO: move the following function to a new module TypeChecking.Overloading
    -- that gathers functions concerning disambiguation of overloading.

    -- | Remember a name disambiguation (during type checking).
    --   To be used later during syntax highlighting.
    --   Also: raise user warnings associated with the name.
    storeDisambiguatedName :: NameKind -> A.QName -> TCM ()
    storeDisambiguatedName :: NameKind -> QName -> TCM ()
    storeDisambiguatedName NameKind
    k QName
    q = do
      QName -> TCM ()
    forall (m :: * -> *).
    (MonadWarning m, ReadTCState m) =>
    QName -> m ()
    raiseWarningsOnUsage QName
    q
      Maybe Key -> (Key -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Range -> Maybe Key
    forall {b} {a}. Num b => Range' a -> Maybe b
    start (Range -> Maybe Key) -> Range -> Maybe Key
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    q) ((Key -> TCM ()) -> TCM ()) -> (Key -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Key
    i ->
        Lens' (IntMap DisambiguatedName) TCState
    -> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (IntMap DisambiguatedName) TCState
    stDisambiguatedNames ((IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ())
    -> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Key
    -> DisambiguatedName
    -> IntMap DisambiguatedName
    -> IntMap DisambiguatedName
    forall a. Key -> a -> IntMap a -> IntMap a
    IntMap.insert Key
    i (DisambiguatedName
     -> IntMap DisambiguatedName -> IntMap DisambiguatedName)
    -> DisambiguatedName
    -> IntMap DisambiguatedName
    -> IntMap DisambiguatedName
    forall a b. (a -> b) -> a -> b
    $ NameKind -> QName -> DisambiguatedName
    DisambiguatedName NameKind
    k QName
    q
      where
      start :: Range' a -> Maybe b
    start Range' a
    r = Int32 -> b
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int32 -> b) -> (Position' () -> Int32) -> Position' () -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Position' () -> Int32
    forall a. Position' a -> Int32
    P.posPos (Position' () -> b) -> Maybe (Position' ()) -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Range' a -> Maybe (Position' ())
    forall a. Range' a -> Maybe (Position' ())
    P.rStart' Range' a
    r

    -- | Store a disambiguation of record field tags for the purpose of highlighting.
    disambiguateRecordFields
      :: [C.Name]   -- ^ Record field names in a record expression.
      -> [A.QName]  -- ^ Record field names in the corresponding record type definition
      -> TCM ()
    disambiguateRecordFields :: [Name] -> [QName] -> TCM ()
    disambiguateRecordFields [Name]
    cxs [QName]
    axs = [Name] -> (Name -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Name]
    cxs ((Name -> TCM ()) -> TCM ()) -> (Name -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Name
    cx -> do
      Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe ((QName -> Bool) -> [QName] -> Maybe QName
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Name
    cx Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Name -> Bool) -> (QName -> Name) -> QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Name
    A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName) [QName]
    axs) (() -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    ax -> do
        QName -> TCM ()
    storeDisambiguatedField QName
    ax{ qnameName :: Name
    A.qnameName = (QName -> Name
    A.qnameName QName
    ax) { nameConcrete :: Name
    A.nameConcrete = Name
    cx } }