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