{-# OPTIONS_GHC -Wunused-imports #-}
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
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]
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