-- | 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 Data.Aeson
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 modFile :: ModuleToSource
modFile (range :: Range
range, aspect :: Aspects
aspect) = [Pair] -> Value
object
  [ "range" Text -> [Int] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= [Range -> Int
from Range
range, Range -> Int
to Range
range]
  , "atoms" Text -> [String] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Aspects -> [String]
toAtoms Aspects
aspect
  , "tokenBased" Text -> TokenBased -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Aspects -> TokenBased
tokenBased Aspects
aspect
  , "note" Text -> Maybe String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Aspects -> Maybe String
note Aspects
aspect
  , "definitionSite" Text -> Maybe Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (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 mdl :: TopLevelModuleName
mdl position :: Int
position _ _) = [Pair] -> Value
object
      [ "filepath" Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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)
      , "position" Text -> Int -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Int
position
      ]

instance EncodeTCM TokenBased where
instance ToJSON TokenBased where
    toJSON :: TokenBased -> Value
toJSON TokenBased = Text -> Value
String "TokenBased"
    toJSON NotOnlyTokenBased = Text -> Value
String "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 info :: HighlightingInfo
info remove :: RemoveTokenBasedHighlighting
remove method :: HighlightingMethod
method modFile :: ModuleToSource
modFile =
  case HighlightingInfo -> HighlightingMethod -> HighlightingMethod
chooseHighlightingMethod HighlightingInfo
info HighlightingMethod
method of
    Direct   -> IO Value
direct
    Indirect -> IO Value
indirect
  where
    result :: Value
    result :: Value
result = [Pair] -> Value
object
      [ "remove" Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= case RemoveTokenBasedHighlighting
remove of
          RemoveHighlighting -> Bool
True
          KeepHighlighting -> Bool
False
      , "payload" Text -> [Value] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= ((Range, Aspects) -> Value) -> [(Range, Aspects)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleToSource -> (Range, Aspects) -> Value
showAspects ModuleToSource
modFile) (HighlightingInfo -> [(Range, Aspects)]
ranges 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
      [ "kind"   Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Text -> Value
String "HighlightingInfo"
      , "direct" Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Bool
True
      , "info"   Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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
        [ "kind"     Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Text -> Value
String "HighlightingInfo"
        , "direct"   Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Bool
False
        , "filepath" Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
filepath
        ]