    -- | 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 -> [FilePath] -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Aspects -> [FilePath]
    toAtoms Aspects
    aspect
      , Text
    "tokenBased" Text -> TokenBased -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Aspects -> TokenBased
    tokenBased Aspects
    aspect
      , Text
    "note" Text -> FilePath -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Aspects -> FilePath
    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 FilePath
    _) = [Pair] -> Value
    object
          [ Text
    "filepath" Text -> FilePath -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= AbsolutePath -> FilePath
    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
          FilePath
    filepath <- FilePath -> IO FilePath
    writeToTempFile (ByteString -> FilePath
    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 -> FilePath -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= FilePath
    filepath
            ]