Agda.Interaction.Highlighting.JSON

Functions which give precise syntax highlighting info in JSON format.

Documentation

jsonifyHighlightingInfo

Arguments

:: HighlightingInfo

-> RemoveTokenBasedHighlighting

-> HighlightingMethod

-> ModuleToSource

Must contain a mapping for every definition site's module.

-> IO Value

Turns syntax highlighting information into a JSON value

Orphan instances

EncodeTCM TokenBased

Methods

encodeTCM :: TokenBased -> TCM Value

ToJSON TokenBased

Methods

toJSON :: TokenBased -> Value

toEncoding :: TokenBased -> Encoding

toJSONList :: [TokenBased] -> Value

toEncodingList :: [TokenBased] -> Encoding

omitField :: TokenBased -> Bool