-- | Functions which give precise syntax highlighting info in JSON format.

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.JSON
import Agda.Interaction.Response
import Agda.TypeChecking.Monad (HighlightingMethod(..), ModuleToSource)
import Agda.Utils.FileName (filePath)
import Agda.Utils.IO.TempFile (writeToTempFile)

import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Map as Map

import Agda.Utils.Impossible

-- | Encode meta information into a JSON Value
showAspects
  :: ModuleToSource
     -- ^ Must contain a mapping for the definition site's module, if any.
  -> (Range, Aspects) -> Value
showAspects :: ModuleToSource -> (Range, Aspects) -> Value
showAspects ModuleToSource
modFile (Range
range, Aspects
aspect) = [Pair] -> Value
object
  [ Text
"range" forall a. ToJSON a => Text -> a -> Pair
.= [Range -> Int
from Range
range, Range -> Int
to Range
range]
  , Text
"atoms" forall a. ToJSON a => Text -> a -> Pair
.= Aspects -> [FilePath]
toAtoms Aspects
aspect
  , Text
"tokenBased" forall a. ToJSON a => Text -> a -> Pair
.= Aspects -> TokenBased
tokenBased Aspects
aspect
  , Text
"note" forall a. ToJSON a => Text -> a -> Pair
.= Aspects -> FilePath
note Aspects
aspect
  , Text
"definitionSite" forall a. ToJSON a => Text -> a -> Pair
.= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinitionSite -> Value
defSite (Aspects -> Maybe DefinitionSite
definitionSite Aspects
aspect)
  ]
  where
    defSite :: DefinitionSite -> Value
defSite (DefinitionSite TopLevelModuleName
mdl Int
position Bool
_ Maybe FilePath
_) = [Pair] -> Value
object
      [ Text
"filepath" forall a. ToJSON a => Text -> a -> Pair
.= AbsolutePath -> FilePath
filePath (forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ TopLevelModuleName
mdl ModuleToSource
modFile)
      , Text
"position" forall a. ToJSON a => Text -> a -> Pair
.= Int
position
      ]

instance EncodeTCM TokenBased where
instance ToJSON TokenBased where
    toJSON :: TokenBased -> Value
toJSON TokenBased
TokenBased = Text -> Value
String Text
"TokenBased"
    toJSON TokenBased
NotOnlyTokenBased = Text -> Value
String Text
"NotOnlyTokenBased"

-- | Turns syntax highlighting information into a JSON value
jsonifyHighlightingInfo
  :: HighlightingInfo
  -> RemoveTokenBasedHighlighting
  -> HighlightingMethod
  -> ModuleToSource
     -- ^ Must contain a mapping for every definition site's module.
  -> IO Value
jsonifyHighlightingInfo :: HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO Value
jsonifyHighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile =
  case HighlightingInfo -> HighlightingMethod -> HighlightingMethod
chooseHighlightingMethod HighlightingInfo
info HighlightingMethod
method of
    HighlightingMethod
Direct   -> IO Value
direct
    HighlightingMethod
Indirect -> IO Value
indirect
  where
    result :: Value
    result :: Value
result = [Pair] -> Value
object
      [ Text
"remove" forall a. ToJSON a => Text -> a -> Pair
.= case RemoveTokenBasedHighlighting
remove of
          RemoveTokenBasedHighlighting
RemoveHighlighting -> Bool
True
          RemoveTokenBasedHighlighting
KeepHighlighting -> Bool
False
      , Text
"payload" forall a. ToJSON a => Text -> a -> Pair
.= forall a b. (a -> b) -> [a] -> [b]
map (ModuleToSource -> (Range, Aspects) -> Value
showAspects ModuleToSource
modFile) (forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList HighlightingInfo
info)
      ]

    direct :: IO Value
    direct :: IO Value
direct = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
object
      [ Text
"kind"   forall a. ToJSON a => Text -> a -> Pair
.= Text -> Value
String Text
"HighlightingInfo"
      , Text
"direct" forall a. ToJSON a => Text -> a -> Pair
.= Bool
True
      , Text
"info"   forall a. ToJSON a => Text -> a -> Pair
.= Value
result
      ]

    indirect :: IO Value
    indirect :: IO Value
indirect = do
      FilePath
filepath <- FilePath -> IO FilePath
writeToTempFile (ByteString -> FilePath
BS.unpack (forall a. ToJSON a => a -> ByteString
encode Value
result))
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
object
        [ Text
"kind"     forall a. ToJSON a => Text -> a -> Pair
.= Text -> Value
String Text
"HighlightingInfo"
        , Text
"direct"   forall a. ToJSON a => Text -> a -> Pair
.= Bool
False
        , Text
"filepath" forall a. ToJSON a => Text -> a -> Pair
.= FilePath
filepath
        ]