module Agda.Utils.String where
import Data.Char
import Data.List
import Numeric
import Agda.Utils.List
quote :: String -> String
quote s = "\"" ++ concatMap escape s ++ "\""
where
escape c | c == '\n' = "\\n"
| c `elem` escapeChars = ['\\', c]
| otherwise = [c]
escapeChars = "\"\\"
showIndex :: (Show i, Integral i) => i -> String
showIndex n =
showIntAtBase 10 (\i -> toEnum (i + fromEnum '\x2080')) n ""
addFinalNewLine :: String -> String
addFinalNewLine "" = "\n"
addFinalNewLine s | last s == '\n' = s
| otherwise = s ++ "\n"
indent :: Integral i => i -> String -> String
indent i = unlines . map (genericReplicate i ' ' ++) . lines
newtype Str = Str { unStr :: String }
deriving Eq
instance Show Str where
show = unStr
showThousandSep :: Show a => a -> String
showThousandSep = reverse . intercalate "," . chop 3 . reverse . show
ltrim :: String -> String
ltrim = dropWhile isSpace
rtrim :: String -> String
rtrim = reverse . ltrim . reverse
trim :: String -> String
trim = rtrim . ltrim