module Agda.Interaction.Highlighting.HTML.Forester
( renderForesterHtml,
)
where
import Data.ByteString (ByteString)
import Data.ByteString qualified as S (isInfixOf)
import Data.List (isInfixOf)
import Data.Monoid (mappend, mempty)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.Encoding (decodeUtf8)
import Data.Text.Lazy qualified as L
import Data.Text.Lazy.Builder (Builder)
import Data.Text.Lazy.Builder qualified as B
import Text.Blaze.Html5 (Html)
import Text.Blaze.Internal
( ChoiceString (..),
MarkupM (..),
StaticString (getText),
)
fromChoiceString ::
(ByteString -> Text) ->
ChoiceString ->
Builder
fromChoiceString :: (ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
_ (Static StaticString
s) = Text -> Builder
B.fromText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ StaticString -> Text
getText StaticString
s
fromChoiceString ByteString -> Text
_ (String [Char]
s) = Text -> Builder
B.fromText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack [Char]
s
fromChoiceString ByteString -> Text
_ (Text Text
s) = Text -> Builder
B.fromText Text
s
fromChoiceString ByteString -> Text
d (ByteString ByteString
s) = Text -> Builder
B.fromText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ ByteString -> Text
d ByteString
s
fromChoiceString ByteString -> Text
d (PreEscaped ChoiceString
x) = case ChoiceString
x of
String [Char]
s -> Text -> Builder
B.fromText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack [Char]
s
Text Text
s -> Text -> Builder
B.fromText Text
s
ChoiceString
s -> (ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
s
fromChoiceString ByteString -> Text
d (External ChoiceString
x) = case ChoiceString
x of
String [Char]
s -> if [Char]
"</" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` [Char]
s then Builder
forall a. Monoid a => a
mempty else Text -> Builder
B.fromText ([Char] -> Text
T.pack [Char]
s)
Text Text
s -> if Text
"</" Text -> Text -> Bool
`T.isInfixOf` Text
s then Builder
forall a. Monoid a => a
mempty else Text -> Builder
B.fromText Text
s
ByteString ByteString
s -> if ByteString
"</" ByteString -> ByteString -> Bool
`S.isInfixOf` ByteString
s then Builder
forall a. Monoid a => a
mempty else Text -> Builder
B.fromText (ByteString -> Text
d ByteString
s)
ChoiceString
s -> (ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
s
fromChoiceString ByteString -> Text
d (AppendChoiceString ChoiceString
x ChoiceString
y) =
(ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
x Builder -> Builder -> Builder
forall a. Monoid a => a -> a -> a
`mappend` (ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
y
fromChoiceString ByteString -> Text
_ ChoiceString
EmptyChoiceString = Builder
forall a. Monoid a => a
mempty
{-# INLINE fromChoiceString #-}
modify_open :: StaticString -> Text
modify_open :: StaticString -> Text
modify_open StaticString
open =
let a :: Text
a = StaticString -> Text
getText StaticString
open
in Char -> Text -> Text
T.cons Char
'<' (Text -> Text -> Text
T.append Text
"html:" (HasCallStack => Text -> Text
Text -> Text
T.tail Text
a))
modify_key :: StaticString -> Text
modify_key :: StaticString -> Text
modify_key StaticString
key =
let a :: Text
a = StaticString -> Text
getText StaticString
key
in Int -> Text -> Text
T.dropEnd Int
2 (Text -> Text
T.strip Text
a)
wrap_verb :: Builder -> Builder
wrap_verb :: Builder -> Builder
wrap_verb Builder
w = Text -> Builder
B.fromLazyText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ (Char -> Text -> Text) -> Text -> Text -> Text
forall a. (Char -> a -> a) -> a -> Text -> a
L.foldr Char -> Text -> Text
go Text
"" (Builder -> Text
B.toLazyText Builder
w)
where
go :: Char -> L.Text -> L.Text
go :: Char -> Text -> Text
go Char
'[' Text
acc = Text -> Text -> Text
L.append Text
"\\startverb[\\stopverb" Text
acc
go Char
']' Text
acc = Text -> Text -> Text
L.append Text
"\\startverb]\\stopverb" Text
acc
go Char
x Text
acc = Char -> Text -> Text
L.cons Char
x Text
acc
renderMarkupBuilderWith ::
(ByteString -> Text) ->
Html ->
Builder
renderMarkupBuilderWith :: (ByteString -> Text) -> Html -> Builder
renderMarkupBuilderWith ByteString -> Text
d = Builder -> Html -> Builder
forall b. Builder -> MarkupM b -> Builder
go Builder
forall a. Monoid a => a
mempty
where
go :: Builder -> MarkupM b -> Builder
go :: forall b. Builder -> MarkupM b -> Builder
go Builder
attrs (Parent StaticString
_ StaticString
open StaticString
close MarkupM b
content) =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Text -> Builder
B.fromText Text
"\\",
Text -> Builder
B.fromText (StaticString -> Text
modify_open StaticString
open),
Text -> Builder
B.fromText Text
">",
Builder
attrs,
Text -> Builder
B.fromText Text
"{",
Builder -> MarkupM b -> Builder
forall b. Builder -> MarkupM b -> Builder
go Builder
forall a. Monoid a => a
mempty MarkupM b
content,
Text -> Builder
B.fromText Text
"}"
]
go Builder
attrs (CustomParent ChoiceString
tag MarkupM b
content) =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Text -> Builder
B.fromText Text
"\\<html:",
(ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
tag,
Text -> Builder
B.fromText Text
">",
Builder
attrs,
Text -> Builder
B.fromText Text
"{",
Builder -> MarkupM b -> Builder
forall b. Builder -> MarkupM b -> Builder
go Builder
forall a. Monoid a => a
mempty MarkupM b
content,
(ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
tag,
Text -> Builder
B.fromText Text
"}"
]
go Builder
attrs (Leaf StaticString
_ StaticString
begin StaticString
end b
_) =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Text -> Builder
B.fromText (StaticString -> Text
modify_open StaticString
begin),
Text -> Builder
B.fromText Text
">",
Builder
attrs,
Text -> Builder
B.fromText Text
"{}"
]
go Builder
attrs (CustomLeaf ChoiceString
tag Bool
close b
_) =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Text -> Builder
B.fromText Text
"\\<html:",
(ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
tag,
Builder
attrs,
Text -> Builder
B.fromText Text
">{}"
]
go Builder
attrs (AddAttribute StaticString
_ StaticString
key ChoiceString
value MarkupM b
h) =
Builder -> MarkupM b -> Builder
forall b. Builder -> MarkupM b -> Builder
go
( [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Char -> Builder
B.singleton Char
'[',
Text -> Builder
B.fromText (StaticString -> Text
modify_key StaticString
key),
Text -> Builder
B.fromText Text
"]{",
Builder -> Builder
wrap_verb ((ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
value),
Text -> Builder
B.fromText Text
"}",
Builder
attrs
]
)
MarkupM b
h
go Builder
attrs (AddCustomAttribute ChoiceString
key ChoiceString
value MarkupM b
h) =
Builder -> MarkupM b -> Builder
forall b. Builder -> MarkupM b -> Builder
go
( [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ Char -> Builder
B.singleton Char
'[',
(ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
key,
Text -> Builder
B.fromText Text
"]{",
Builder -> Builder
wrap_verb ((ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
value),
Text -> Builder
B.fromText Text
"}",
Builder
attrs
]
)
MarkupM b
h
go Builder
_ (Content ChoiceString
content b
_) = Builder -> Builder
wrap_verb ((ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
content)
go Builder
_ (Comment ChoiceString
comment b
_) = Text -> Builder
B.fromText Text
"% " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (ByteString -> Text) -> ChoiceString -> Builder
fromChoiceString ByteString -> Text
d ChoiceString
comment
go Builder
attrs (Append MarkupM b
h1 MarkupM b
h2) = Builder -> MarkupM b -> Builder
forall b. Builder -> MarkupM b -> Builder
go Builder
attrs MarkupM b
h1 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> MarkupM b -> Builder
forall b. Builder -> MarkupM b -> Builder
go Builder
attrs MarkupM b
h2
go Builder
_ (Empty b
_) = Builder
forall a. Monoid a => a
mempty
{-# NOINLINE go #-}
{-# INLINE renderMarkupBuilderWith #-}
renderMarkupWith :: (ByteString -> Text) -> Html -> L.Text
renderMarkupWith :: (ByteString -> Text) -> Html -> Text
renderMarkupWith ByteString -> Text
d = Builder -> Text
B.toLazyText (Builder -> Text) -> (Html -> Builder) -> Html -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString -> Text) -> Html -> Builder
renderMarkupBuilderWith ByteString -> Text
d
{-# INLINE renderMarkupWith #-}
renderForesterHtml :: Html -> L.Text
renderForesterHtml :: Html -> Text
renderForesterHtml = (ByteString -> Text) -> Html -> Text
renderMarkupWith ByteString -> Text
decodeUtf8
{-# INLINE renderForesterHtml #-}