module Agda.Utils.String where
import Data.Char
import qualified Data.List as List
import Numeric
import Agda.Utils.List
import Data.IORef
import Agda.Interaction.Options.IORefs (unicodeOrAscii, UnicodeOrAscii(..))
import qualified System.IO.Unsafe as UNSAFE
quote :: String -> String
quote s = "\"" ++ concatMap escape s ++ "\""
where
escape c | c == '\n' = "\\n"
| c `elem` escapeChars = ['\\', c]
| otherwise = [c]
escapeChars :: String
escapeChars = "\"\\"
haskellStringLiteral :: String -> String
haskellStringLiteral s = "\"" ++ concatMap escape s ++ "\""
where
escape c | c == '\n' = "\\n"
| c == '"' = "\\\""
| c == '\\' = "\\\\"
| ok c = [c]
| otherwise = [c]
ok c = case generalCategory c of
UppercaseLetter -> True
LowercaseLetter -> True
TitlecaseLetter -> True
_ -> isSymbol c || isPunctuation c
delimiter :: String -> String
delimiter s = concat [ replicate 4 '\x2014'
, " ", s, " "
, replicate (54 - length s) '\x2014'
]
showIndex :: (Show i, Integral i) => i -> String
showIndex n =
let opt = UNSAFE.unsafePerformIO (readIORef unicodeOrAscii) in
case opt of
UnicodeOk -> showIntAtBase 10 (\i -> toEnum (i + fromEnum '\x2080')) n ""
AsciiOnly -> show 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 (List.genericReplicate i ' ' ++) . lines
newtype Str = Str { unStr :: String }
deriving Eq
instance Show Str where
show = unStr
showThousandSep :: Show a => a -> String
showThousandSep = reverse . List.intercalate "," . chop 3 . reverse . show
ltrim :: String -> String
ltrim = dropWhile isSpace
rtrim :: String -> String
rtrim = List.dropWhileEnd isSpace
trim :: String -> String
trim = rtrim . ltrim