module Render.Literal where
import Agda.Syntax.Literal ( Literal(..), showChar', showText )
import Render.Class
import Render.RichText
import Render.Name ()
import Render.Common ()
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