Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Concrete.Glyph

Description

Choice of Unicode or ASCII glyphs.

Synopsis

data UnicodeOrAscii
- = UnicodeOk
- | AsciiOnly
unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO ()
specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters
braces' :: Doc -> Doc
dbraces :: Doc -> Doc
forallQ :: Doc
leftIdiomBrkt :: Doc
rightIdiomBrkt :: Doc
emptyIdiomBrkt :: Doc
arrow :: Doc
lambda :: Doc
data SpecialCharacters = SpecialCharacters {
- _dbraces :: Doc -> Doc
- _lambda :: Doc
- _arrow :: Doc
- _forallQ :: Doc
- _leftIdiomBrkt :: Doc
- _rightIdiomBrkt :: Doc
- _emptyIdiomBrkt :: Doc
}

Documentation

data UnicodeOrAscii Source #

We want to know whether we are allowed to insert unicode characters or not.

Constructors

UnicodeOk
AsciiOnly

Instances

Instances details

EmbPrj UnicodeOrAscii Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UnicodeOrAscii -> S Int32 Source # icod_ :: UnicodeOrAscii -> S Int32 Source # value :: Int32 -> R UnicodeOrAscii Source #
Bounded UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods minBound :: UnicodeOrAscii # maxBound :: UnicodeOrAscii #
Enum UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods succ :: UnicodeOrAscii -> UnicodeOrAscii # pred :: UnicodeOrAscii -> UnicodeOrAscii # toEnum :: Int -> UnicodeOrAscii # fromEnum :: UnicodeOrAscii -> Int # enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii] # enumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] # enumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] # enumFromThenTo :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] #
Generic UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Associated Types type Rep UnicodeOrAscii :: Type -> Type # Methods from :: UnicodeOrAscii -> Rep UnicodeOrAscii x # to :: Rep UnicodeOrAscii x -> UnicodeOrAscii #
Show UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods showsPrec :: Int -> UnicodeOrAscii -> ShowS # show :: UnicodeOrAscii -> String # showList :: [UnicodeOrAscii] -> ShowS #
NFData UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods rnf :: UnicodeOrAscii -> () #
Eq UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods (==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool # (/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool #
type Rep UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO () Source #

specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters Source #

Return the glyph set based on a given (unicode or ascii) glyph mode

braces' :: Doc -> Doc Source #

dbraces :: Doc -> Doc Source #

forallQ :: Doc Source #

leftIdiomBrkt :: Doc Source #

rightIdiomBrkt :: Doc Source #

emptyIdiomBrkt :: Doc Source #

arrow :: Doc Source #

lambda :: Doc Source #

data SpecialCharacters Source #

Picking the appropriate set of special characters depending on whether we are allowed to use unicode or have to limit ourselves to ascii.

Constructors

SpecialCharacters
Fields _dbraces :: Doc -> Doc _lambda :: Doc _arrow :: Doc _forallQ :: Doc _leftIdiomBrkt :: Doc _rightIdiomBrkt :: Doc _emptyIdiomBrkt :: Doc