1{-| Choice of Unicode or ASCII glyphs. 2-} 3module Agda.Syntax.Concrete.Glyph 4 ( UnicodeOrAscii(..) 5 , unsafeSetUnicodeOrAscii 6 , specialCharactersForGlyphs 7 , braces', dbraces 8 , forallQ 9 , leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt 10 , arrow, lambda 11 , SpecialCharacters(..) 12 ) where 13 14import Control.DeepSeq 15 16import Data.IORef (IORef, newIORef, readIORef, writeIORef) 17import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO) 18 19import GHC.Generics (Generic) 20 21import Agda.Utils.List 22import Agda.Utils.Null 23import Agda.Utils.Pretty 24 25-- | We want to know whether we are allowed to insert unicode characters or not. 26data UnicodeOrAscii 27 = UnicodeOk 28 | AsciiOnly 29 deriving (Show, Eq, Enum, Bounded, Generic) 30 31instance NFData UnicodeOrAscii 32 33{-# NOINLINE unsafeUnicodeOrAsciiIORef #-} 34unsafeUnicodeOrAsciiIORef :: IORef UnicodeOrAscii 35unsafeUnicodeOrAsciiIORef = UNSAFE.unsafePerformIO $ newIORef UnicodeOk 36 37{-# NOINLINE unsafeSetUnicodeOrAscii #-} 38unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO () 39unsafeSetUnicodeOrAscii = writeIORef unsafeUnicodeOrAsciiIORef 40 41-- | Are we allowed to use unicode supscript characters? 42unsafeUnicodeOrAscii :: UnicodeOrAscii 43unsafeUnicodeOrAscii = UNSAFE.unsafePerformIO (readIORef unsafeUnicodeOrAsciiIORef) 44 45-- | Picking the appropriate set of special characters depending on 46-- whether we are allowed to use unicode or have to limit ourselves 47-- to ascii. 48 49data SpecialCharacters = SpecialCharacters 50 { _dbraces :: Doc -> Doc 51 , _lambda :: Doc 52 , _arrow :: Doc 53 , _forallQ :: Doc 54 , _leftIdiomBrkt :: Doc 55 , _rightIdiomBrkt :: Doc 56 , _emptyIdiomBrkt :: Doc 57 } 58 59specialCharactersUnicode :: SpecialCharacters 60specialCharactersUnicode = SpecialCharacters 61 { _dbraces = (("\x2983 " <>) . (<> " \x2984")) 62 , _lambda = "\x03bb" 63 , _arrow = "\x2192" 64 , _forallQ = "\x2200" 65 , _leftIdiomBrkt = "\x2987" 66 , _rightIdiomBrkt = "\x2988" 67 , _emptyIdiomBrkt = "\x2987\x2988" 68 } 69 70specialCharactersAscii :: SpecialCharacters 71specialCharactersAscii = SpecialCharacters 72 { _dbraces = braces . braces' 73 , _lambda = "\\" 74 , _arrow = "->" 75 , _forallQ = "forall" 76 , _leftIdiomBrkt = "(|" 77 , _rightIdiomBrkt = "|)" 78 , _emptyIdiomBrkt = "(|)" 79 } 80 81-- | Return the glyph set based on a given (unicode or ascii) glyph mode 82specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters 83specialCharactersForGlyphs UnicodeOk = specialCharactersUnicode 84specialCharactersForGlyphs AsciiOnly = specialCharactersAscii 85 86-- | Choose the glyph set based on the unsafe IORef. 87{-# NOINLINE specialCharacters #-} 88specialCharacters :: SpecialCharacters 89specialCharacters = specialCharactersForGlyphs unsafeUnicodeOrAscii 90 91braces' :: Doc -> Doc 92braces' d = caseList (render d) (braces d) {-else-} $ \ c cs -> 93 braces (spaceIfDash c <> d <> spaceIfDash (last1 c cs)) 94 -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269) 95 -- Andreas, 2018-07-21, #3161: Also avoid ending a comment 96 where 97 spaceIfDash '-' = " " 98 spaceIfDash _ = empty 99 100-- double braces... 101dbraces :: Doc -> Doc 102dbraces = _dbraces specialCharacters 103 104-- forall quantifier 105forallQ :: Doc 106forallQ = _forallQ specialCharacters 107 108-- left, right, and empty idiom bracket 109leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Doc 110leftIdiomBrkt = _leftIdiomBrkt specialCharacters 111rightIdiomBrkt = _rightIdiomBrkt specialCharacters 112emptyIdiomBrkt = _emptyIdiomBrkt specialCharacters 113 114arrow, lambda :: Doc 115arrow = _arrow specialCharacters 116lambda = _lambda specialCharacters 117