{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}

module Render.RichText
  ( Block(..),
    Inlines (..),
    -- LinkTarget (..),
    space,
    text,
    text',
    parens,
    -- link,
    linkRange,
    linkHole,
    icon,
    -- combinators
    (<+>),
    punctuate,
    braces,
    braces',
    dbraces,
    mparens,
    hcat,
    hsep,
    sep,
    fsep,
    vcat,
    fcat,
    -- symbols
    arrow,
    lambda,
    forallQ,
    showIndex,
    leftIdiomBrkt,
    rightIdiomBrkt,
    emptyIdiomBrkt,
  )
where

-- import qualified Agda.Interaction.Options   as Agda
-- import qualified Agda.Syntax.Concrete.Glyph as Agda
import qualified Agda.Syntax.Position       as Agda
import qualified Agda.Utils.FileName        as Agda
import qualified Agda.Utils.Null            as Agda
import           Agda.Utils.Suffix (toSubscriptDigit)

import           Data.Aeson (ToJSON (toJSON), Value (Null))
import           Data.Foldable (toList)
import           Data.Sequence (Seq (..))
import qualified Data.Sequence     as Seq
import           Data.String (IsString (..))
import qualified Data.Strict.Maybe as Strict

import           GHC.Generics (Generic)

--------------------------------------------------------------------------------
-- | Block elements

data Block
  -- for blocks like "Goal" & "Have"
  = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String
  -- for ordinary goals & context
  | Unlabeled Inlines (Maybe String) (Maybe Agda.Range)
  -- headers
  | Header String
  deriving ((forall x. Block -> Rep Block x)
-> (forall x. Rep Block x -> Block) -> Generic Block
forall x. Rep Block x -> Block
forall x. Block -> Rep Block x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Block -> Rep Block x
from :: forall x. Block -> Rep Block x
$cto :: forall x. Rep Block x -> Block
to :: forall x. Rep Block x -> Block
Generic)

instance ToJSON Block

--------------------------------------------------------------------------------

newtype Inlines = Inlines {Inlines -> Seq Inline
unInlines :: Seq Inline}

-- Represent Inlines with String literals
instance IsString Inlines where
  fromString :: String -> Inlines
fromString String
s = Seq Inline -> Inlines
Inlines (Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (String -> ClassNames -> Inline
Text String
s ClassNames
forall a. Monoid a => a
mempty))

instance Semigroup Inlines where
  Inlines Seq Inline
as <> :: Inlines -> Inlines -> Inlines
<> Inlines Seq Inline
bs = Seq Inline -> Inlines
Inlines (Seq Inline -> Seq Inline -> Seq Inline
merge Seq Inline
as Seq Inline
bs)
    where
      merge :: Seq Inline -> Seq Inline -> Seq Inline
      merge :: Seq Inline -> Seq Inline -> Seq Inline
merge Seq Inline
Empty      Seq Inline
ys = Seq Inline
ys
      merge (Seq Inline
xs :|> Inline
x) Seq Inline
ys = Seq Inline -> Seq Inline -> Seq Inline
merge Seq Inline
xs (Inline -> Seq Inline -> Seq Inline
cons Inline
x Seq Inline
ys)

      cons :: Inline -> Seq Inline -> Seq Inline
      cons :: Inline -> Seq Inline -> Seq Inline
cons (Text String
s ClassNames
c) (Text String
t ClassNames
d :<| Seq Inline
xs)
        -- merge 2 adjacent Text if they have the same classnames
        | ClassNames
c ClassNames -> ClassNames -> Bool
forall a. Eq a => a -> a -> Bool
== ClassNames
d    = String -> ClassNames -> Inline
Text (String
s String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
t) ClassNames
c Inline -> Seq Inline -> Seq Inline
forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs
        | Bool
otherwise = String -> ClassNames -> Inline
Text String
s ClassNames
c Inline -> Seq Inline -> Seq Inline
forall a. a -> Seq a -> Seq a
:<| String -> ClassNames -> Inline
Text String
t ClassNames
d Inline -> Seq Inline -> Seq Inline
forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs
      cons (Text String
s ClassNames
c) (Horz [] :<| Seq Inline
xs) = Inline -> Seq Inline -> Seq Inline
cons (String -> ClassNames -> Inline
Text String
s ClassNames
c) Seq Inline
xs
      cons (Text String
s ClassNames
c) (Horz (Inlines Seq Inline
t:[Inlines]
ts) :<| Seq Inline
xs)
        -- merge Text with Horz when possible
        = [Inlines] -> Inline
Horz (Seq Inline -> Inlines
Inlines (Inline -> Seq Inline -> Seq Inline
cons (String -> ClassNames -> Inline
Text String
s ClassNames
c) Seq Inline
t) Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
:[Inlines]
ts) Inline -> Seq Inline -> Seq Inline
forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs
      cons Inline
x Seq Inline
xs = Inline
x Inline -> Seq Inline -> Seq Inline
forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs


instance Monoid Inlines where
  mempty :: Inlines
mempty = Seq Inline -> Inlines
Inlines Seq Inline
forall a. Monoid a => a
mempty

instance ToJSON Inlines where
  toJSON :: Inlines -> Value
toJSON (Inlines Seq Inline
xs) = Seq Inline -> Value
forall a. ToJSON a => a -> Value
toJSON Seq Inline
xs

instance Show Inlines where
  show :: Inlines -> String
show (Inlines Seq Inline
xs) = ClassNames -> String
unwords (ClassNames -> String) -> ClassNames -> String
forall a b. (a -> b) -> a -> b
$ (Inline -> String) -> [Inline] -> ClassNames
forall a b. (a -> b) -> [a] -> [b]
map Inline -> String
forall a. Show a => a -> String
show ([Inline] -> ClassNames) -> [Inline] -> ClassNames
forall a b. (a -> b) -> a -> b
$ Seq Inline -> [Inline]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Inline
xs

-- | see if the rendered text is "empty"
isEmpty :: Inlines -> Bool
isEmpty :: Inlines -> Bool
isEmpty (Inlines Seq Inline
elems) = (Inline -> Bool) -> ViewL Inline -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inline -> Bool
elemIsEmpty (Seq Inline -> ViewL Inline
forall a. Seq a -> ViewL a
Seq.viewl Seq Inline
elems)
  where
    elemIsEmpty :: Inline -> Bool
    elemIsEmpty :: Inline -> Bool
elemIsEmpty (Icon String
_ ClassNames
_) = Bool
False
    elemIsEmpty (Text String
"" ClassNames
_) = Bool
True
    elemIsEmpty (Text String
_ ClassNames
_) = Bool
False
    elemIsEmpty (Link Range
_ Inlines
xs ClassNames
_) = (Inline -> Bool) -> Seq Inline -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inline -> Bool
elemIsEmpty (Seq Inline -> Bool) -> Seq Inline -> Bool
forall a b. (a -> b) -> a -> b
$ Inlines -> Seq Inline
unInlines Inlines
xs
    elemIsEmpty (Hole Int
_) = Bool
False
    elemIsEmpty (Horz [Inlines]
xs) = (Inlines -> Bool) -> [Inlines] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inlines -> Bool
isEmpty [Inlines]
xs
    elemIsEmpty (Vert [Inlines]
xs) = (Inlines -> Bool) -> [Inlines] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inlines -> Bool
isEmpty [Inlines]
xs
    elemIsEmpty (Parn Inlines
_) = Bool
False
    elemIsEmpty (PrHz [Inlines]
_) = Bool
False

infixr 6 <+>

(<+>) :: Inlines -> Inlines -> Inlines
Inlines
x <+> :: Inlines -> Inlines -> Inlines
<+> Inlines
y
  | Inlines -> Bool
isEmpty Inlines
x = Inlines
y
  | Inlines -> Bool
isEmpty Inlines
y = Inlines
x
  | Bool
otherwise = Inlines
x Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
" " Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
y

-- | Whitespace
space :: Inlines
space :: Inlines
space = Inlines
" "

text :: String -> Inlines
text :: String -> Inlines
text String
s = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ String -> ClassNames -> Inline
Text String
s ClassNames
forall a. Monoid a => a
mempty

text' :: ClassNames -> String -> Inlines
text' :: ClassNames -> String -> Inlines
text' ClassNames
cs String
s = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ String -> ClassNames -> Inline
Text String
s ClassNames
cs

-- When there's only 1 Horz inside a Parn, convert it to PrHz
parens :: Inlines -> Inlines
parens :: Inlines -> Inlines
parens (Inlines (Horz [Inlines]
xs :<| Seq Inline
Empty)) = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inline
PrHz [Inlines]
xs
parens Inlines
others = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ Inlines -> Inline
Parn Inlines
others

icon :: String -> Inlines
icon :: String -> Inlines
icon String
s = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ String -> ClassNames -> Inline
Icon String
s []

linkRange :: Agda.Range -> Inlines -> Inlines
linkRange :: Range -> Inlines -> Inlines
linkRange Range
range Inlines
xs = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ Range -> Inlines -> ClassNames -> Inline
Link Range
range Inlines
xs ClassNames
forall a. Monoid a => a
mempty

linkHole :: Int -> Inlines
linkHole :: Int -> Inlines
linkHole Int
i = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines) -> Seq Inline -> Inlines
forall a b. (a -> b) -> a -> b
$ Inline -> Seq Inline
forall a. a -> Seq a
Seq.singleton (Inline -> Seq Inline) -> Inline -> Seq Inline
forall a b. (a -> b) -> a -> b
$ Int -> Inline
Hole Int
i

--------------------------------------------------------------------------------

type ClassNames = [String]

--------------------------------------------------------------------------------

-- | Internal type, to be converted to JSON values
data Inline
  = Icon String ClassNames
  | Text String ClassNames
  | Link Agda.Range Inlines ClassNames
  | Hole Int
  | -- | Horizontal grouping, wrap when there's no space
    Horz [Inlines]
  | -- | Vertical grouping, each children would end with a newline
    Vert [Inlines]
  | -- | Parenthese
    Parn Inlines
  | -- | Parenthese around a Horizontal, special case
    PrHz [Inlines]
  deriving ((forall x. Inline -> Rep Inline x)
-> (forall x. Rep Inline x -> Inline) -> Generic Inline
forall x. Rep Inline x -> Inline
forall x. Inline -> Rep Inline x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Inline -> Rep Inline x
from :: forall x. Inline -> Rep Inline x
$cto :: forall x. Rep Inline x -> Inline
to :: forall x. Rep Inline x -> Inline
Generic)

instance ToJSON Inline

instance Show Inline where
  show :: Inline -> String
show (Icon String
s ClassNames
_) = String
s
  show (Text String
s ClassNames
_) = String
s
  show (Link Range
_ Inlines
xs ClassNames
_) = ClassNames -> String
forall a. Monoid a => [a] -> a
mconcat ((Inline -> String) -> [Inline] -> ClassNames
forall a b. (a -> b) -> [a] -> [b]
map Inline -> String
forall a. Show a => a -> String
show ([Inline] -> ClassNames) -> [Inline] -> ClassNames
forall a b. (a -> b) -> a -> b
$ Seq Inline -> [Inline]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq Inline -> [Inline]) -> Seq Inline -> [Inline]
forall a b. (a -> b) -> a -> b
$ Inlines -> Seq Inline
unInlines Inlines
xs)
  show (Hole Int
i) = String
"?" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (Horz [Inlines]
xs) = ClassNames -> String
unwords ((Inlines -> String) -> [Inlines] -> ClassNames
forall a b. (a -> b) -> [a] -> [b]
map Inlines -> String
forall a. Show a => a -> String
show ([Inlines] -> ClassNames) -> [Inlines] -> ClassNames
forall a b. (a -> b) -> a -> b
$ [Inlines] -> [Inlines]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [Inlines]
xs)
  show (Vert [Inlines]
xs) = ClassNames -> String
unlines ((Inlines -> String) -> [Inlines] -> ClassNames
forall a b. (a -> b) -> [a] -> [b]
map Inlines -> String
forall a. Show a => a -> String
show ([Inlines] -> ClassNames) -> [Inlines] -> ClassNames
forall a b. (a -> b) -> a -> b
$ [Inlines] -> [Inlines]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [Inlines]
xs)
  show (Parn Inlines
x) = String
"(" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Inlines -> String
forall a. Show a => a -> String
show Inlines
x String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (PrHz [Inlines]
xs) = String
"(" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ClassNames -> String
unwords ((Inlines -> String) -> [Inlines] -> ClassNames
forall a b. (a -> b) -> [a] -> [b]
map Inlines -> String
forall a. Show a => a -> String
show ([Inlines] -> ClassNames) -> [Inlines] -> ClassNames
forall a b. (a -> b) -> a -> b
$ [Inlines] -> [Inlines]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [Inlines]
xs) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"

--------------------------------------------------------------------------------

-- | ToJSON instances for A.types
instance {-# OVERLAPS #-} ToJSON Agda.Range

instance ToJSON (Agda.Interval' ()) where
  toJSON :: IntervalWithoutFile -> Value
toJSON (Agda.Interval Position' ()
start Position' ()
end) = (Position' (), Position' ()) -> Value
forall a. ToJSON a => a -> Value
toJSON (Position' ()
start, Position' ()
end)

instance ToJSON (Agda.Position' ()) where
  toJSON :: Position' () -> Value
toJSON (Agda.Pn () Int32
pos Int32
line Int32
col) = [Int32] -> Value
forall a. ToJSON a => a -> Value
toJSON [Int32
line, Int32
col, Int32
pos]

instance {-# OVERLAPS #-} ToJSON Agda.SrcFile where
  toJSON :: Maybe RangeFile -> Value
toJSON Maybe RangeFile
Strict.Nothing = Value
Null
  toJSON (Strict.Just RangeFile
path) = RangeFile -> Value
forall a. ToJSON a => a -> Value
toJSON RangeFile
path

instance ToJSON Agda.AbsolutePath where
  toJSON :: AbsolutePath -> Value
toJSON (Agda.AbsolutePath Text
path) = Text -> Value
forall a. ToJSON a => a -> Value
toJSON Text
path

#if MIN_VERSION_Agda(2,6,3)
instance ToJSON Agda.RangeFile where
  toJSON :: RangeFile -> Value
toJSON (Agda.RangeFile AbsolutePath
path Maybe TopLevelModuleName
_maybeTopLevelModuleName) = AbsolutePath -> Value
forall a. ToJSON a => a -> Value
toJSON AbsolutePath
path
#endif

--------------------------------------------------------------------------------

-- | Utilities / Combinators

-- -- TODO: implement this
-- indent :: Inlines -> Inlines
-- indent x = "  " <> x

punctuate :: Inlines -> [Inlines] -> [Inlines]
punctuate :: Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
_ [] = []
punctuate Inlines
delim [Inlines]
xs = (Inlines -> Inlines -> Inlines)
-> [Inlines] -> [Inlines] -> [Inlines]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
(<>) [Inlines]
xs (Int -> Inlines -> [Inlines]
forall a. Int -> a -> [a]
replicate ([Inlines] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Inlines]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Inlines
delim [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ [Inlines
forall a. Monoid a => a
mempty])

--------------------------------------------------------------------------------

-- | Just pure concatenation, no grouping or whatsoever
hcat :: [Inlines] -> Inlines
hcat :: [Inlines] -> Inlines
hcat = [Inlines] -> Inlines
forall a. Monoid a => [a] -> a
mconcat

hsep :: [Inlines] -> Inlines
hsep :: [Inlines] -> Inlines
hsep [] = Inlines
forall a. Monoid a => a
mempty
hsep [Inlines
x] = Inlines
x
hsep (Inlines
x : [Inlines]
xs) = Inlines
x Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
hsep [Inlines]
xs

--------------------------------------------------------------------------------

-- | Vertical listing
vcat :: [Inlines] -> Inlines
vcat :: [Inlines] -> Inlines
vcat = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines)
-> ([Inlines] -> Seq Inline) -> [Inlines] -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inline -> Seq Inline
forall a. a -> Seq a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inline -> Seq Inline)
-> ([Inlines] -> Inline) -> [Inlines] -> Seq Inline
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Inlines] -> Inline
Vert

-- | Horizontal listing
sep :: [Inlines] -> Inlines
sep :: [Inlines] -> Inlines
sep = Seq Inline -> Inlines
Inlines (Seq Inline -> Inlines)
-> ([Inlines] -> Seq Inline) -> [Inlines] -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inline -> Seq Inline
forall a. a -> Seq a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inline -> Seq Inline)
-> ([Inlines] -> Inline) -> [Inlines] -> Seq Inline
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Inlines] -> Inline
Horz

fsep :: [Inlines] -> Inlines
fsep :: [Inlines] -> Inlines
fsep = [Inlines] -> Inlines
sep

fcat :: [Inlines] -> Inlines
fcat :: [Inlines] -> Inlines
fcat = [Inlines] -> Inlines
sep

--------------------------------------------------------------------------------

-- | Single braces
braces :: Inlines -> Inlines
braces :: Inlines -> Inlines
braces Inlines
x = Inlines
"{" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
x Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"}"

-- | Double braces
dbraces :: Inlines -> Inlines
dbraces :: Inlines -> Inlines
dbraces = SpecialCharacters -> Inlines -> Inlines
_dbraces SpecialCharacters
specialCharacters

arrow :: Inlines
arrow :: Inlines
arrow = SpecialCharacters -> Inlines
_arrow SpecialCharacters
specialCharacters

lambda :: Inlines
lambda :: Inlines
lambda = SpecialCharacters -> Inlines
_lambda SpecialCharacters
specialCharacters

forallQ :: Inlines
forallQ :: Inlines
forallQ = SpecialCharacters -> Inlines
_forallQ SpecialCharacters
specialCharacters

-- left, right, and empty idiom bracket
leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Inlines
leftIdiomBrkt :: Inlines
leftIdiomBrkt = SpecialCharacters -> Inlines
_leftIdiomBrkt SpecialCharacters
specialCharacters
rightIdiomBrkt :: Inlines
rightIdiomBrkt = SpecialCharacters -> Inlines
_rightIdiomBrkt SpecialCharacters
specialCharacters
emptyIdiomBrkt :: Inlines
emptyIdiomBrkt = SpecialCharacters -> Inlines
_emptyIdiomBrkt SpecialCharacters
specialCharacters

-- | Apply 'parens' to 'Doc' if boolean is true.
mparens :: Bool -> Inlines -> Inlines
mparens :: Bool -> Inlines -> Inlines
mparens Bool
True = Inlines -> Inlines
parens
mparens Bool
False = Inlines -> Inlines
forall a. a -> a
id

-- | From braces'
braces' :: Inlines -> Inlines
braces' :: Inlines -> Inlines
braces' Inlines
d =
  let s :: String
s = Inlines -> String
forall a. Show a => a -> String
show Inlines
d
   in if String -> Bool
forall a. Null a => a -> Bool
Agda.null String
s
        then Inlines -> Inlines
braces Inlines
d
        else Inlines -> Inlines
braces (Char -> Inlines
forall {a}. (IsString a, Monoid a) => Char -> a
spaceIfDash (String -> Char
forall a. HasCallStack => [a] -> a
head String
s) Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
d Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Char -> Inlines
forall {a}. (IsString a, Monoid a) => Char -> a
spaceIfDash (String -> Char
forall a. HasCallStack => [a] -> a
last String
s))
  where
    -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
    -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
    spaceIfDash :: Char -> a
spaceIfDash Char
'-' = a
" "
    spaceIfDash Char
_ = a
forall a. Monoid a => a
mempty

-- | Shows a non-negative integer using the characters ₀-₉ instead of
-- 0-9 unless the user explicitly asked us to not use any unicode characters.
showIndex :: (Show i, Integral i) => i -> String
showIndex :: forall i. (Show i, Integral i) => i -> String
showIndex = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toSubscriptDigit (String -> String) -> (i -> String) -> i -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> String
forall a. Show a => a -> String
show

--------------------------------------------------------------------------------
--
-- | Picking the appropriate set of special characters depending on
-- whether we are allowed to use unicode or have to limit ourselves
-- to ascii.
data SpecialCharacters = SpecialCharacters
  { SpecialCharacters -> Inlines -> Inlines
_dbraces :: Inlines -> Inlines,
    SpecialCharacters -> Inlines
_lambda :: Inlines,
    SpecialCharacters -> Inlines
_arrow :: Inlines,
    SpecialCharacters -> Inlines
_forallQ :: Inlines,
    SpecialCharacters -> Inlines
_leftIdiomBrkt :: Inlines,
    SpecialCharacters -> Inlines
_rightIdiomBrkt :: Inlines,
    SpecialCharacters -> Inlines
_emptyIdiomBrkt :: Inlines
  }

{-# NOINLINE specialCharacters #-}
specialCharacters :: SpecialCharacters
specialCharacters :: SpecialCharacters
specialCharacters =
  SpecialCharacters
    { _dbraces :: Inlines -> Inlines
_dbraces = (Inlines
"\x2983 " Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<>) (Inlines -> Inlines) -> (Inlines -> Inlines) -> Inlines -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
" \x2984"),
      _lambda :: Inlines
_lambda = Inlines
"\x03bb",
      _arrow :: Inlines
_arrow = Inlines
"\x2192",
      _forallQ :: Inlines
_forallQ = Inlines
"\x2200",
      _leftIdiomBrkt :: Inlines
_leftIdiomBrkt = Inlines
"\x2987",
      _rightIdiomBrkt :: Inlines
_rightIdiomBrkt = Inlines
"\x2988",
      _emptyIdiomBrkt :: Inlines
_emptyIdiomBrkt = Inlines
"\x2987\x2988"
    }