    -- | Common syntax highlighting functions for Emacs and JSON

    module Agda.Interaction.Highlighting.Common
      ( toAtoms
      , chooseHighlightingMethod
      ) where

    import Agda.Interaction.Highlighting.Precise
    import Agda.Syntax.Common
    import Agda.TypeChecking.Monad (HighlightingMethod(..))
    import Data.Maybe (maybeToList)
    import Data.Char (toLower)
    import qualified Data.Set as Set

    -- | Converts the 'aspect' and 'otherAspects' fields to strings that are
    -- friendly to editors.
    toAtoms :: Aspects -> [String]
    toAtoms :: Aspects -> [String]
    toAtoms Aspects
    m = (OtherAspect -> String) -> [OtherAspect] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map OtherAspect -> String
    forall a. Show a => a -> String
    toAtom (Set OtherAspect -> [OtherAspect]
    forall a. Set a -> [a]
    Set.toList (Set OtherAspect -> [OtherAspect])
    -> Set OtherAspect -> [OtherAspect]
    forall a b. (a -> b) -> a -> b
    $ Aspects -> Set OtherAspect
    otherAspects Aspects
    m)
             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ Maybe Aspect -> [String]
    toAtoms' (Aspects -> Maybe Aspect
    aspect Aspects
    m)
      where

      toAtom :: Show a => a -> String
      toAtom :: forall a. Show a => a -> String
    toAtom = (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower (String -> String) -> (a -> String) -> a -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> String
    forall a. Show a => a -> String
    show

      kindToAtom :: NameKind -> String
    kindToAtom (Constructor Induction
    Inductive)   = String
    "inductiveconstructor"
      kindToAtom (Constructor Induction
    CoInductive) = String
    "coinductiveconstructor"
      kindToAtom NameKind
    k                         = NameKind -> String
    forall a. Show a => a -> String
    toAtom NameKind
    k

      toAtoms' :: Maybe Aspect -> [String]
    toAtoms' Maybe Aspect
    Nothing               = []
      toAtoms' (Just (Name Maybe NameKind
    mKind Bool
    op)) =
        (NameKind -> String) -> [NameKind] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map NameKind -> String
    kindToAtom (Maybe NameKind -> [NameKind]
    forall a. Maybe a -> [a]
    maybeToList Maybe NameKind
    mKind) [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    opAtom
        where opAtom :: [String]
    opAtom | Bool
    op        = [String
    "operator"]
                     | Bool
    otherwise = []
      toAtoms' (Just Aspect
    a) = [Aspect -> String
    forall a. Show a => a -> String
    toAtom Aspect
    a]

    -- | Choose which method to use based on HighlightingInfo and HighlightingMethod
    chooseHighlightingMethod
      :: HighlightingInfo
      -> HighlightingMethod
      -> HighlightingMethod
    chooseHighlightingMethod :: HighlightingInfo -> HighlightingMethod -> HighlightingMethod
    chooseHighlightingMethod HighlightingInfo
    info HighlightingMethod
    method = case HighlightingInfo -> [(Range, Aspects)]
    forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
    toList HighlightingInfo
    info of
      [(Range, Aspects)]
    _             | HighlightingMethod
    method HighlightingMethod -> HighlightingMethod -> Bool
    forall a. Eq a => a -> a -> Bool
    == HighlightingMethod
    Direct -> HighlightingMethod
    Direct
      ((Range
    _, Aspects
    mi) : [(Range, Aspects)]
    _) | Aspects -> Bool
    check Aspects
    mi         -> HighlightingMethod
    Direct
      [(Range, Aspects)]
    _                                -> HighlightingMethod
    Indirect

      where check :: Aspects -> Bool
    check Aspects
    mi = Aspects -> Set OtherAspect
    otherAspects Aspects
    mi Set OtherAspect -> Set OtherAspect -> Bool
    forall a. Eq a => a -> a -> Bool
    == OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    TypeChecks
                    Bool -> Bool -> Bool
    || Aspects
    mi Aspects -> Aspects -> Bool
    forall a. Eq a => a -> a -> Bool
    == Aspects
    forall a. Monoid a => a
    mempty