{-# LANGUAGE CPP #-}
module Agda.Interaction.Highlighting.JSON (jsonifyHighlightingInfo) where
import Agda.Interaction.Highlighting.Common
import Agda.Interaction.Highlighting.Precise hiding (String)
import Agda.Interaction.Highlighting.Range (Range(..))
import Agda.Interaction.Response
import Agda.TypeChecking.Monad (HighlightingMethod(..), ModuleToSource)
import Agda.Utils.FileName (filePath)
import Agda.Utils.IO.TempFile (writeToTempFile)
import Data.Aeson
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Map as Map
#include "undefined.h"
import Agda.Utils.Impossible
showAspects
:: ModuleToSource
-> (Range, Aspects) -> Value
showAspects modFile (range, aspect) = object
[ "range" .= [from range, to range]
, "atoms" .= toAtoms aspect
, "tokenBased" .= tokenBased aspect
, "note" .= note aspect
, "definitionSite" .= fmap defSite (definitionSite aspect)
]
where
defSite (DefinitionSite mdl position _ _) = object
[ "filepath" .= filePath (Map.findWithDefault __IMPOSSIBLE__ mdl modFile)
, "position" .= position
]
instance ToJSON TokenBased where
toJSON TokenBased = String "TokenBased"
toJSON NotOnlyTokenBased = String "NotOnlyTokenBased"
jsonifyHighlightingInfo
:: HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO Value
jsonifyHighlightingInfo info remove method modFile =
case chooseHighlightingMethod info method of
Direct -> direct
Indirect -> indirect
where
result :: Value
result = object
[ "remove" .= case remove of
RemoveHighlighting -> True
KeepHighlighting -> False
, "payload" .= map (showAspects modFile) (ranges info)
]
direct :: IO Value
direct = return $ object
[ "kind" .= String "HighlightingInfo"
, "direct" .= True
, "info" .= result
]
indirect :: IO Value
indirect = do
filepath <- writeToTempFile (BS.unpack (encode result))
return $ object
[ "kind" .= String "HighlightingInfo"
, "direct" .= False
, "filepath" .= filepath
]