-- | 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" Text -> [Int] -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= [Range -> Int
from Range
range, Range -> Int
to Range
range]
  , Text
"atoms" Text -> [String] -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Aspects -> [String]
toAtoms Aspects
aspect
  , Text
"tokenBased" Text -> TokenBased -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Aspects -> TokenBased
tokenBased Aspects
aspect
  , Text
"note" Text -> String -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Aspects -> String
note Aspects
aspect
  , Text
"definitionSite" Text -> Maybe Value -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= (DefinitionSite -> Value) -> Maybe DefinitionSite -> Maybe Value
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 String
_) = [Pair] -> Value
object
      [ Text
"filepath" Text -> String -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= AbsolutePath -> String
filePath (AbsolutePath
-> TopLevelModuleName -> ModuleToSource -> AbsolutePath
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ TopLevelModuleName
mdl ModuleToSource
modFile)
      , Text
"position" Text -> Int -> Pair
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" Text -> Bool -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= case RemoveTokenBasedHighlighting
remove of
          RemoveTokenBasedHighlighting
RemoveHighlighting -> Bool
True
          RemoveTokenBasedHighlighting
KeepHighlighting -> Bool
False
      , Text
"payload" Text -> [Value] -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= ((Range, Aspects) -> Value) -> [(Range, Aspects)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleToSource -> (Range, Aspects) -> Value
showAspects ModuleToSource
modFile) (HighlightingInfo -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList HighlightingInfo
info)
      ]

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

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