-- | 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
toAtom (forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Aspects -> Set OtherAspect
otherAspects Aspects
m)
         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 = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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                         = 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)) =
    forall a b. (a -> b) -> [a] -> [b]
map NameKind -> String
kindToAtom (forall a. Maybe a -> [a]
maybeToList Maybe NameKind
mKind) forall a. [a] -> [a] -> [a]
++ [String]
opAtom
    where opAtom :: [String]
opAtom | Bool
op        = [String
"operator"]
                 | Bool
otherwise = []
  toAtoms' (Just Aspect
a) = [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 forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList HighlightingInfo
info of
  [(Range, Aspects)]
_             | HighlightingMethod
method 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 forall a. Eq a => a -> a -> Bool
== forall a. a -> Set a
Set.singleton OtherAspect
TypeChecks
                Bool -> Bool -> Bool
|| Aspects
mi forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty