module Render.Literal where

import Agda.Syntax.Literal ( Literal(..), showChar', showText )
import Render.Class
import Render.RichText
import Render.Name ()
import Render.Common ()

--------------------------------------------------------------------------------

-- | Literal
instance Render Literal where
  render :: Literal -> Inlines
render (LitNat Integer
n)    = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Integer
n
  render (LitWord64 Word64
n) = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Word64
n
  render (LitFloat Double
d)  = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Double
d
  render (LitString Text
s) = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ Text -> ShowS
showText Text
s [Char]
""
  render (LitChar Char
c)   = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
"'" forall a. [a] -> [a] -> [a]
++ Char -> ShowS
showChar' Char
c [Char]
"'"
  render (LitQName QName
x)  = forall a. Render a => a -> Inlines
render QName
x
  render (LitMeta AbsolutePath
_ MetaId
x) = forall a. Render a => a -> Inlines
render MetaId
x