{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Interaction.Highlighting.HTML.Base
( HtmlOptions(..)
, HtmlHighlight(..)
, prepareCommonDestinationAssets
, srcFileOfInterface
, defaultPageGen
, MonadLogHtml(logHtml)
, LogHtmlT
, runLogHtmlWith
) where
import Prelude hiding ((!!), concatMap)
import Control.DeepSeq
import Control.Monad
import Control.Monad.Trans ( MonadIO(..), lift )
import Control.Monad.Trans.Reader ( ReaderT(runReaderT), ask )
import Data.Function ( on )
import Data.Foldable (toList, concatMap)
import Data.Maybe
import qualified Data.IntMap as IntMap
import Data.List.Split (splitWhen)
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
import GHC.Generics (Generic)
import qualified Network.URI.Encode
import System.FilePath
import System.Directory
import Text.Blaze.Html5
( preEscapedToHtml
, toHtml
, stringValue
, Html
, (!)
, Attribute
)
import qualified Text.Blaze.Html5 as Html5
import qualified Text.Blaze.Html5.Attributes as Attr
import Text.Blaze.Html.Renderer.Text ( renderHtml )
import Paths_Agda
import Agda.Interaction.Highlighting.Precise hiding (toList)
import Agda.Syntax.Common
import Agda.Syntax.TopLevelModuleName
import qualified Agda.TypeChecking.Monad as TCM
( Interface(..)
)
import Agda.Utils.Function
import Agda.Utils.List1 (String1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Syntax.Common.Pretty
import Agda.Utils.Impossible
htmlDataDir :: FilePath
htmlDataDir :: [Char]
htmlDataDir = [Char]
"html"
defaultCSSFile :: FilePath
defaultCSSFile :: [Char]
defaultCSSFile = [Char]
"Agda.css"
occurrenceHighlightJsFile :: FilePath
occurrenceHighlightJsFile :: [Char]
occurrenceHighlightJsFile = [Char]
"highlight-hover.js"
rstDelimiter :: String
rstDelimiter :: [Char]
rstDelimiter = [Char]
".. raw:: html\n"
orgDelimiterStart :: String
orgDelimiterStart :: [Char]
orgDelimiterStart = [Char]
"#+BEGIN_EXPORT html\n<pre class=\"Agda\">\n"
orgDelimiterEnd :: String
orgDelimiterEnd :: [Char]
orgDelimiterEnd = [Char]
"</pre>\n#+END_EXPORT\n"
data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
deriving (Key -> HtmlHighlight -> ShowS
[HtmlHighlight] -> ShowS
HtmlHighlight -> [Char]
(Key -> HtmlHighlight -> ShowS)
-> (HtmlHighlight -> [Char])
-> ([HtmlHighlight] -> ShowS)
-> Show HtmlHighlight
forall a.
(Key -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Key -> HtmlHighlight -> ShowS
showsPrec :: Key -> HtmlHighlight -> ShowS
$cshow :: HtmlHighlight -> [Char]
show :: HtmlHighlight -> [Char]
$cshowList :: [HtmlHighlight] -> ShowS
showList :: [HtmlHighlight] -> ShowS
Show, HtmlHighlight -> HtmlHighlight -> Bool
(HtmlHighlight -> HtmlHighlight -> Bool)
-> (HtmlHighlight -> HtmlHighlight -> Bool) -> Eq HtmlHighlight
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HtmlHighlight -> HtmlHighlight -> Bool
== :: HtmlHighlight -> HtmlHighlight -> Bool
$c/= :: HtmlHighlight -> HtmlHighlight -> Bool
/= :: HtmlHighlight -> HtmlHighlight -> Bool
Eq, (forall x. HtmlHighlight -> Rep HtmlHighlight x)
-> (forall x. Rep HtmlHighlight x -> HtmlHighlight)
-> Generic HtmlHighlight
forall x. Rep HtmlHighlight x -> HtmlHighlight
forall x. HtmlHighlight -> Rep HtmlHighlight x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HtmlHighlight -> Rep HtmlHighlight x
from :: forall x. HtmlHighlight -> Rep HtmlHighlight x
$cto :: forall x. Rep HtmlHighlight x -> HtmlHighlight
to :: forall x. Rep HtmlHighlight x -> HtmlHighlight
Generic)
instance NFData HtmlHighlight
highlightOnlyCode :: HtmlHighlight -> FileType -> Bool
highlightOnlyCode :: HtmlHighlight -> FileType -> Bool
highlightOnlyCode HtmlHighlight
HighlightAll FileType
_ = Bool
False
highlightOnlyCode HtmlHighlight
HighlightCode FileType
_ = Bool
True
highlightOnlyCode HtmlHighlight
HighlightAuto FileType
AgdaFileType = Bool
False
highlightOnlyCode HtmlHighlight
HighlightAuto FileType
MdFileType = Bool
True
highlightOnlyCode HtmlHighlight
HighlightAuto FileType
RstFileType = Bool
True
highlightOnlyCode HtmlHighlight
HighlightAuto FileType
OrgFileType = Bool
True
highlightOnlyCode HtmlHighlight
HighlightAuto FileType
TypstFileType = Bool
True
highlightOnlyCode HtmlHighlight
HighlightAuto FileType
TexFileType = Bool
False
highlightedFileExt :: HtmlHighlight -> FileType -> String
highlightedFileExt :: HtmlHighlight -> FileType -> [Char]
highlightedFileExt HtmlHighlight
hh FileType
ft
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ HtmlHighlight -> FileType -> Bool
highlightOnlyCode HtmlHighlight
hh FileType
ft = [Char]
"html"
| Bool
otherwise = case FileType
ft of
FileType
AgdaFileType -> [Char]
"html"
FileType
MdFileType -> [Char]
"md"
FileType
RstFileType -> [Char]
"rst"
FileType
TexFileType -> [Char]
"tex"
FileType
OrgFileType -> [Char]
"org"
FileType
TypstFileType -> [Char]
"typ"
data HtmlOptions = HtmlOptions
{ HtmlOptions -> [Char]
htmlOptDir :: FilePath
, HtmlOptions -> HtmlHighlight
htmlOptHighlight :: HtmlHighlight
, HtmlOptions -> Bool
htmlOptHighlightOccurrences :: Bool
, HtmlOptions -> Maybe [Char]
htmlOptCssFile :: Maybe FilePath
} deriving HtmlOptions -> HtmlOptions -> Bool
(HtmlOptions -> HtmlOptions -> Bool)
-> (HtmlOptions -> HtmlOptions -> Bool) -> Eq HtmlOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HtmlOptions -> HtmlOptions -> Bool
== :: HtmlOptions -> HtmlOptions -> Bool
$c/= :: HtmlOptions -> HtmlOptions -> Bool
/= :: HtmlOptions -> HtmlOptions -> Bool
Eq
data HtmlInputSourceFile = HtmlInputSourceFile
{ HtmlInputSourceFile -> TopLevelModuleName
_srcFileModuleName :: TopLevelModuleName
, HtmlInputSourceFile -> FileType
_srcFileType :: FileType
, HtmlInputSourceFile -> Text
_srcFileText :: Text
, HtmlInputSourceFile -> HighlightingInfo
_srcFileHighlightInfo :: HighlightingInfo
}
srcFileOfInterface ::
TopLevelModuleName -> TCM.Interface -> HtmlInputSourceFile
srcFileOfInterface :: TopLevelModuleName -> Interface -> HtmlInputSourceFile
srcFileOfInterface TopLevelModuleName
m Interface
i = TopLevelModuleName
-> FileType -> Text -> HighlightingInfo -> HtmlInputSourceFile
HtmlInputSourceFile TopLevelModuleName
m (Interface -> FileType
TCM.iFileType Interface
i) (Interface -> Text
TCM.iSource Interface
i) (Interface -> HighlightingInfo
TCM.iHighlighting Interface
i)
type HtmlLogMessage = String
type HtmlLogAction m = HtmlLogMessage -> m ()
class MonadLogHtml m where
logHtml :: HtmlLogAction m
type LogHtmlT m = ReaderT (HtmlLogAction m) m
instance Monad m => MonadLogHtml (LogHtmlT m) where
logHtml :: HtmlLogAction (LogHtmlT m)
logHtml [Char]
message = do
HtmlLogAction m
doLog <- ReaderT (HtmlLogAction m) m (HtmlLogAction m)
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
m () -> LogHtmlT m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT (HtmlLogAction m) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> LogHtmlT m ()) -> m () -> LogHtmlT m ()
forall a b. (a -> b) -> a -> b
$ HtmlLogAction m
doLog [Char]
message
runLogHtmlWith :: Monad m => HtmlLogAction m -> LogHtmlT m a -> m a
runLogHtmlWith :: forall (m :: * -> *) a.
Monad m =>
HtmlLogAction m -> LogHtmlT m a -> m a
runLogHtmlWith = (LogHtmlT m a -> HtmlLogAction m -> m a)
-> HtmlLogAction m -> LogHtmlT m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip LogHtmlT m a -> HtmlLogAction m -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
renderSourceFile :: HtmlOptions -> HtmlInputSourceFile -> Text
renderSourceFile :: HtmlOptions -> HtmlInputSourceFile -> Text
renderSourceFile HtmlOptions
opts = HtmlInputSourceFile -> Text
renderSourcePage
where
cssFile :: [Char]
cssFile = [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
defaultCSSFile (HtmlOptions -> Maybe [Char]
htmlOptCssFile HtmlOptions
opts)
highlightOccur :: Bool
highlightOccur = HtmlOptions -> Bool
htmlOptHighlightOccurrences HtmlOptions
opts
htmlHighlight :: HtmlHighlight
htmlHighlight = HtmlOptions -> HtmlHighlight
htmlOptHighlight HtmlOptions
opts
renderSourcePage :: HtmlInputSourceFile -> Text
renderSourcePage (HtmlInputSourceFile TopLevelModuleName
moduleName FileType
fileType Text
sourceCode HighlightingInfo
hinfo) =
[Char] -> Bool -> Bool -> TopLevelModuleName -> Html -> Text
page [Char]
cssFile Bool
highlightOccur Bool
onlyCode TopLevelModuleName
moduleName Html
pageContents
where
tokens :: [TokenInfo]
tokens = Text -> HighlightingInfo -> [TokenInfo]
tokenStream Text
sourceCode HighlightingInfo
hinfo
onlyCode :: Bool
onlyCode = HtmlHighlight -> FileType -> Bool
highlightOnlyCode HtmlHighlight
htmlHighlight FileType
fileType
pageContents :: Html
pageContents = Bool -> FileType -> [TokenInfo] -> Html
code Bool
onlyCode FileType
fileType [TokenInfo]
tokens
defaultPageGen :: (MonadIO m, MonadLogHtml m) => HtmlOptions -> HtmlInputSourceFile -> m ()
defaultPageGen :: forall (m :: * -> *).
(MonadIO m, MonadLogHtml m) =>
HtmlOptions -> HtmlInputSourceFile -> m ()
defaultPageGen HtmlOptions
opts srcFile :: HtmlInputSourceFile
srcFile@(HtmlInputSourceFile TopLevelModuleName
moduleName FileType
ft Text
_ HighlightingInfo
_) = do
HtmlLogAction m
forall (m :: * -> *). MonadLogHtml m => HtmlLogAction m
logHtml HtmlLogAction m -> HtmlLogAction m
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (Doc Aspects -> [Char]) -> Doc Aspects -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"Generating HTML for" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> TopLevelModuleName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty TopLevelModuleName
moduleName Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> ((Doc Aspects -> Doc Aspects
parens ([Char] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [Char]
target)) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects
".")
Text -> HtmlLogAction m
forall (m :: * -> *). MonadIO m => Text -> [Char] -> m ()
writeRenderedHtml Text
html [Char]
target
where
ext :: [Char]
ext = HtmlHighlight -> FileType -> [Char]
highlightedFileExt (HtmlOptions -> HtmlHighlight
htmlOptHighlight HtmlOptions
opts) FileType
ft
target :: [Char]
target = (HtmlOptions -> [Char]
htmlOptDir HtmlOptions
opts) [Char] -> ShowS
</> TopLevelModuleName -> ShowS
modToFile TopLevelModuleName
moduleName [Char]
ext
html :: Text
html = HtmlOptions -> HtmlInputSourceFile -> Text
renderSourceFile HtmlOptions
opts HtmlInputSourceFile
srcFile
prepareCommonDestinationAssets :: MonadIO m => HtmlOptions -> m ()
prepareCommonDestinationAssets :: forall (m :: * -> *). MonadIO m => HtmlOptions -> m ()
prepareCommonDestinationAssets HtmlOptions
options = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
let htmlDir :: [Char]
htmlDir = HtmlOptions -> [Char]
htmlOptDir HtmlOptions
options
Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True [Char]
htmlDir
let cssFile :: Maybe [Char]
cssFile = HtmlOptions -> Maybe [Char]
htmlOptCssFile HtmlOptions
options
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe [Char] -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe [Char] -> Bool) -> Maybe [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe [Char]
cssFile) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[Char]
defCssFile <- [Char] -> IO [Char]
getDataFileName ([Char] -> IO [Char]) -> [Char] -> IO [Char]
forall a b. (a -> b) -> a -> b
$
[Char]
htmlDataDir [Char] -> ShowS
</> [Char]
defaultCSSFile
[Char] -> [Char] -> IO ()
copyFile [Char]
defCssFile ([Char]
htmlDir [Char] -> ShowS
</> [Char]
defaultCSSFile)
let highlightOccurrences :: Bool
highlightOccurrences = HtmlOptions -> Bool
htmlOptHighlightOccurrences HtmlOptions
options
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
highlightOccurrences (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[Char]
highlightJsFile <- [Char] -> IO [Char]
getDataFileName ([Char] -> IO [Char]) -> [Char] -> IO [Char]
forall a b. (a -> b) -> a -> b
$
[Char]
htmlDataDir [Char] -> ShowS
</> [Char]
occurrenceHighlightJsFile
[Char] -> [Char] -> IO ()
copyFile [Char]
highlightJsFile ([Char]
htmlDir [Char] -> ShowS
</> [Char]
occurrenceHighlightJsFile)
modToFile :: TopLevelModuleName -> String -> FilePath
modToFile :: TopLevelModuleName -> ShowS
modToFile TopLevelModuleName
m [Char]
ext = ShowS
Network.URI.Encode.encode ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (TopLevelModuleName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty TopLevelModuleName
m) [Char] -> ShowS
<.> [Char]
ext
writeRenderedHtml
:: MonadIO m
=> Text
-> FilePath
-> m ()
writeRenderedHtml :: forall (m :: * -> *). MonadIO m => Text -> [Char] -> m ()
writeRenderedHtml Text
html [Char]
target = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text -> IO ()
UTF8.writeTextToFile [Char]
target Text
html
(!!) :: Html -> [Attribute] -> Html
Html
h !! :: Html -> [Attribute] -> Html
!! [Attribute]
as = Html
h Html -> Attribute -> Html
forall h. Attributable h => h -> Attribute -> h
! [Attribute] -> Attribute
forall a. Monoid a => [a] -> a
mconcat [Attribute]
as
page :: FilePath
-> Bool
-> Bool
-> TopLevelModuleName
-> Html
-> Text
page :: [Char] -> Bool -> Bool -> TopLevelModuleName -> Html -> Text
page [Char]
css
Bool
highlightOccurrences
Bool
htmlHighlight
TopLevelModuleName
modName
Html
pageContent =
Html -> Text
renderHtml (Html -> Text) -> Html -> Text
forall a b. (a -> b) -> a -> b
$ if Bool
htmlHighlight
then Html
pageContent
else Html -> Html
Html5.docTypeHtml (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ Html
hdr Html -> Html -> Html
forall a. Semigroup a => a -> a -> a
<> Html
rest
where
hdr :: Html
hdr = Html -> Html
Html5.head (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat
[ Html
Html5.meta Html -> [Attribute] -> Html
!! [ AttributeValue -> Attribute
Attr.charset AttributeValue
"utf-8" ]
, Html -> Html
Html5.title ([Char] -> Html
forall a. ToMarkup a => a -> Html
toHtml ([Char] -> Html) -> (Doc Aspects -> [Char]) -> Doc Aspects -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (Doc Aspects -> Html) -> Doc Aspects -> Html
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty TopLevelModuleName
modName)
, Html
Html5.link Html -> [Attribute] -> Html
!! [ AttributeValue -> Attribute
Attr.rel AttributeValue
"stylesheet"
, AttributeValue -> Attribute
Attr.href (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ [Char] -> AttributeValue
stringValue [Char]
css
]
, if Bool
highlightOccurrences
then Html -> Html
Html5.script Html
forall a. Monoid a => a
mempty Html -> [Attribute] -> Html
!!
[ AttributeValue -> Attribute
Attr.type_ AttributeValue
"text/javascript"
, AttributeValue -> Attribute
Attr.src (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ [Char] -> AttributeValue
stringValue [Char]
occurrenceHighlightJsFile
]
else Html
forall a. Monoid a => a
mempty
]
rest :: Html
rest = Html -> Html
Html5.body (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ (Html -> Html
Html5.pre (Html -> Html) -> Attribute -> Html -> Html
forall h. Attributable h => h -> Attribute -> h
! AttributeValue -> Attribute
Attr.class_ AttributeValue
"Agda") Html
pageContent
type TokenInfo =
( Int
, String1
, Aspects
)
tokenStream
:: Text
-> HighlightingInfo
-> [TokenInfo]
tokenStream :: Text -> HighlightingInfo -> [TokenInfo]
tokenStream Text
contents HighlightingInfo
info =
(NonEmpty (Maybe Aspects, (Key, Char)) -> TokenInfo)
-> [NonEmpty (Maybe Aspects, (Key, Char))] -> [TokenInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((Maybe Aspects
mi, (Key
pos, Char
c)) :| [(Maybe Aspects, (Key, Char))]
xs) ->
(Key
pos, Char
c Char -> [Char] -> String1
forall a. a -> [a] -> NonEmpty a
:| ((Maybe Aspects, (Key, Char)) -> Char)
-> [(Maybe Aspects, (Key, Char))] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map ((Key, Char) -> Char
forall a b. (a, b) -> b
snd ((Key, Char) -> Char)
-> ((Maybe Aspects, (Key, Char)) -> (Key, Char))
-> (Maybe Aspects, (Key, Char))
-> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Aspects, (Key, Char)) -> (Key, Char)
forall a b. (a, b) -> b
snd) [(Maybe Aspects, (Key, Char))]
xs, Aspects -> Maybe Aspects -> Aspects
forall a. a -> Maybe a -> a
fromMaybe Aspects
forall a. Monoid a => a
mempty Maybe Aspects
mi)) ([NonEmpty (Maybe Aspects, (Key, Char))] -> [TokenInfo])
-> [NonEmpty (Maybe Aspects, (Key, Char))] -> [TokenInfo]
forall a b. (a -> b) -> a -> b
$
((Maybe Aspects, (Key, Char))
-> (Maybe Aspects, (Key, Char)) -> Bool)
-> [(Maybe Aspects, (Key, Char))]
-> [NonEmpty (Maybe Aspects, (Key, Char))]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (Maybe Aspects -> Maybe Aspects -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Maybe Aspects -> Maybe Aspects -> Bool)
-> ((Maybe Aspects, (Key, Char)) -> Maybe Aspects)
-> (Maybe Aspects, (Key, Char))
-> (Maybe Aspects, (Key, Char))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Maybe Aspects, (Key, Char)) -> Maybe Aspects
forall a b. (a, b) -> a
fst) ([(Maybe Aspects, (Key, Char))]
-> [NonEmpty (Maybe Aspects, (Key, Char))])
-> [(Maybe Aspects, (Key, Char))]
-> [NonEmpty (Maybe Aspects, (Key, Char))]
forall a b. (a -> b) -> a -> b
$
(Key -> Char -> (Maybe Aspects, (Key, Char)))
-> [Key] -> [Char] -> [(Maybe Aspects, (Key, Char))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Key
pos Char
c -> (Key -> IntMap Aspects -> Maybe Aspects
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
pos IntMap Aspects
infoMap, (Key
pos, Char
c))) [Key
1..] (Text -> [Char]
T.unpack Text
contents)
where
infoMap :: IntMap Aspects
infoMap = HighlightingInfo -> IntMap Aspects
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap HighlightingInfo
info
code :: Bool
-> FileType
-> [TokenInfo]
-> Html
code :: Bool -> FileType -> [TokenInfo] -> Html
code Bool
onlyCode FileType
fileType = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> ([TokenInfo] -> [Html]) -> [TokenInfo] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
onlyCode
then case FileType
fileType of
FileType
RstFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkRst ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
FileType
MdFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkMd ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
FileType
AgdaFileType -> (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
mkHtml
FileType
OrgFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkOrg ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
FileType
TexFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkMd ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
FileType
TypstFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkMd ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
else (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
mkHtml
where
trd :: (a, b, c) -> c
trd (a
_, b
_, c
a) = c
a
splitByMarkup :: [TokenInfo] -> [[TokenInfo]]
splitByMarkup :: [TokenInfo] -> [[TokenInfo]]
splitByMarkup = (TokenInfo -> Bool) -> [TokenInfo] -> [[TokenInfo]]
forall a. (a -> Bool) -> [a] -> [[a]]
splitWhen ((TokenInfo -> Bool) -> [TokenInfo] -> [[TokenInfo]])
-> (TokenInfo -> Bool) -> [TokenInfo] -> [[TokenInfo]]
forall a b. (a -> b) -> a -> b
$ (Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Markup) (Maybe Aspect -> Bool)
-> (TokenInfo -> Maybe Aspect) -> TokenInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aspects -> Maybe Aspect
aspect (Aspects -> Maybe Aspect)
-> (TokenInfo -> Aspects) -> TokenInfo -> Maybe Aspect
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TokenInfo -> Aspects
forall {a} {b} {c}. (a, b, c) -> c
trd
mkHtml :: TokenInfo -> Html
mkHtml :: TokenInfo -> Html
mkHtml (Key
pos, String1
s, Aspects
mi) =
Bool -> (Html -> Html) -> Html -> Html
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Aspects
mi Aspects -> Aspects -> Bool
forall a. Eq a => a -> a -> Bool
== Aspects
forall a. Monoid a => a
mempty) (Key -> Aspects -> Html -> Html
annotate Key
pos Aspects
mi) (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ [Char] -> Html
forall a. ToMarkup a => a -> Html
toHtml ([Char] -> Html) -> [Char] -> Html
forall a b. (a -> b) -> a -> b
$ String1 -> [Item String1]
forall l. IsList l => l -> [Item l]
List1.toList String1
s
backgroundOrAgdaToHtml :: TokenInfo -> Html
backgroundOrAgdaToHtml :: TokenInfo -> Html
backgroundOrAgdaToHtml token :: TokenInfo
token@(Key
_, String1
s, Aspects
mi) = case Aspects -> Maybe Aspect
aspect Aspects
mi of
Just Aspect
Background -> [Char] -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml ([Char] -> Html) -> [Char] -> Html
forall a b. (a -> b) -> a -> b
$ String1 -> [Item String1]
forall l. IsList l => l -> [Item l]
List1.toList String1
s
Just Aspect
Markup -> Html
forall a. HasCallStack => a
__IMPOSSIBLE__
Maybe Aspect
_ -> TokenInfo -> Html
mkHtml TokenInfo
token
mkRst :: [TokenInfo] -> Html
mkRst :: [TokenInfo] -> Html
mkRst = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> ([TokenInfo] -> [Html]) -> [TokenInfo] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Html
forall a. ToMarkup a => a -> Html
toHtml [Char]
rstDelimiter Html -> [Html] -> [Html]
forall a. a -> [a] -> [a]
:) ([Html] -> [Html])
-> ([TokenInfo] -> [Html]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
backgroundOrAgdaToHtml
mkMd :: [TokenInfo] -> Html
mkMd :: [TokenInfo] -> Html
mkMd [TokenInfo]
tokens = if Bool
containsCode then Html
formatCode else Html
formatNonCode
where
containsCode :: Bool
containsCode = (TokenInfo -> Bool) -> [TokenInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
/= Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Background) (Maybe Aspect -> Bool)
-> (TokenInfo -> Maybe Aspect) -> TokenInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aspects -> Maybe Aspect
aspect (Aspects -> Maybe Aspect)
-> (TokenInfo -> Aspects) -> TokenInfo -> Maybe Aspect
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TokenInfo -> Aspects
forall {a} {b} {c}. (a, b, c) -> c
trd) [TokenInfo]
tokens
formatCode :: Html
formatCode = Html -> Html
Html5.pre (Html -> Html) -> Attribute -> Html -> Html
forall h. Attributable h => h -> Attribute -> h
! AttributeValue -> Attribute
Attr.class_ AttributeValue
"Agda" (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$ TokenInfo -> Html
backgroundOrAgdaToHtml (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
tokens
formatNonCode :: Html
formatNonCode = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$ TokenInfo -> Html
backgroundOrAgdaToHtml (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
tokens
mkOrg :: [TokenInfo] -> Html
mkOrg :: [TokenInfo] -> Html
mkOrg [TokenInfo]
tokens = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$ if Bool
containsCode then [Html]
formatCode else [Html]
formatNonCode
where
containsCode :: Bool
containsCode = (TokenInfo -> Bool) -> [TokenInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
/= Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Background) (Maybe Aspect -> Bool)
-> (TokenInfo -> Maybe Aspect) -> TokenInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aspects -> Maybe Aspect
aspect (Aspects -> Maybe Aspect)
-> (TokenInfo -> Aspects) -> TokenInfo -> Maybe Aspect
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TokenInfo -> Aspects
forall {a} {b} {c}. (a, b, c) -> c
trd) [TokenInfo]
tokens
startDelimiter :: Html
startDelimiter = [Char] -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml [Char]
orgDelimiterStart
endDelimiter :: Html
endDelimiter = [Char] -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml [Char]
orgDelimiterEnd
formatCode :: [Html]
formatCode = Html
startDelimiter Html -> [Html] -> [Html]
forall a. a -> [a] -> [a]
: (TokenInfo -> [Html] -> [Html]) -> [Html] -> [TokenInfo] -> [Html]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\TokenInfo
x -> (TokenInfo -> Html
backgroundOrAgdaToHtml TokenInfo
x Html -> [Html] -> [Html]
forall a. a -> [a] -> [a]
:)) [Html
endDelimiter] [TokenInfo]
tokens
formatNonCode :: [Html]
formatNonCode = (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
backgroundOrAgdaToHtml [TokenInfo]
tokens
annotate :: Int -> Aspects -> Html -> Html
annotate :: Key -> Aspects -> Html -> Html
annotate Key
pos Aspects
mi =
Bool -> (Html -> Html) -> Html -> Html
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
hereAnchor ([Attribute] -> Html -> Html
anchorage [Attribute]
nameAttributes Html
forall a. Monoid a => a
mempty Html -> Html -> Html
forall a. Semigroup a => a -> a -> a
<>) (Html -> Html) -> (Html -> Html) -> Html -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Attribute] -> Html -> Html
anchorage [Attribute]
posAttributes
where
anchorage :: [Attribute] -> Html -> Html
anchorage :: [Attribute] -> Html -> Html
anchorage [Attribute]
attrs Html
html = Html -> Html
Html5.a Html
html Html -> [Attribute] -> Html
!! [Attribute]
attrs
posAttributes :: [Attribute]
posAttributes :: [Attribute]
posAttributes = [[Attribute]] -> [Attribute]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [AttributeValue -> Attribute
Attr.id (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ [Char] -> AttributeValue
stringValue ([Char] -> AttributeValue) -> [Char] -> AttributeValue
forall a b. (a -> b) -> a -> b
$ Key -> [Char]
forall a. Show a => a -> [Char]
show Key
pos ]
, Maybe Attribute -> [Attribute]
forall a. Maybe a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Maybe Attribute -> [Attribute]) -> Maybe Attribute -> [Attribute]
forall a b. (a -> b) -> a -> b
$ DefinitionSite -> Attribute
link (DefinitionSite -> Attribute)
-> Maybe DefinitionSite -> Maybe Attribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi
, AttributeValue -> Attribute
Attr.class_ ([Char] -> AttributeValue
stringValue ([Char] -> AttributeValue) -> [Char] -> AttributeValue
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]]
classes) Attribute -> [()] -> [Attribute]
forall a b. a -> [b] -> [a]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
classes)
]
nameAttributes :: [Attribute]
nameAttributes :: [Attribute]
nameAttributes = [ AttributeValue -> Attribute
Attr.id (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ [Char] -> AttributeValue
stringValue ([Char] -> AttributeValue) -> [Char] -> AttributeValue
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Char] -> [Char]) -> Maybe [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Maybe [Char]
mDefSiteAnchor ]
classes :: [[Char]]
classes = [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ (Char -> [[Char]]) -> [Char] -> [[Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [[Char]]
forall {p} {a}. p -> [a]
noteClasses (Aspects -> [Char]
note Aspects
mi)
, [OtherAspect] -> [[Char]]
otherAspectClasses (Set OtherAspect -> [OtherAspect]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Set OtherAspect -> [OtherAspect])
-> Set OtherAspect -> [OtherAspect]
forall a b. (a -> b) -> a -> b
$ Aspects -> Set OtherAspect
otherAspects Aspects
mi)
, (Aspect -> [[Char]]) -> Maybe Aspect -> [[Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Aspect -> [[Char]]
aspectClasses (Aspects -> Maybe Aspect
aspect Aspects
mi)
]
aspectClasses :: Aspect -> [[Char]]
aspectClasses (Name Maybe NameKind
mKind Bool
op) = [[Char]]
kindClass [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
opClass
where
kindClass :: [[Char]]
kindClass = Maybe [Char] -> [[Char]]
forall a. Maybe a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Maybe [Char] -> [[Char]]) -> Maybe [Char] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (NameKind -> [Char]) -> Maybe NameKind -> Maybe [Char]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameKind -> [Char]
showKind Maybe NameKind
mKind
showKind :: NameKind -> [Char]
showKind (Constructor Induction
Inductive) = [Char]
"InductiveConstructor"
showKind (Constructor Induction
CoInductive) = [Char]
"CoinductiveConstructor"
showKind NameKind
k = NameKind -> [Char]
forall a. Show a => a -> [Char]
show NameKind
k
opClass :: [[Char]]
opClass = [[Char]
"Operator" | Bool
op]
aspectClasses Aspect
a = [Aspect -> [Char]
forall a. Show a => a -> [Char]
show Aspect
a]
otherAspectClasses :: [OtherAspect] -> [[Char]]
otherAspectClasses = (OtherAspect -> [Char]) -> [OtherAspect] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> [Char]
forall a. Show a => a -> [Char]
show
noteClasses :: p -> [a]
noteClasses p
_s = []
hereAnchor :: Bool
hereAnchor :: Bool
hereAnchor = Bool
here Bool -> Bool -> Bool
&& Maybe [Char] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [Char]
mDefSiteAnchor
mDefinitionSite :: Maybe DefinitionSite
mDefinitionSite :: Maybe DefinitionSite
mDefinitionSite = Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi
here :: Bool
here :: Bool
here = Bool -> (DefinitionSite -> Bool) -> Maybe DefinitionSite -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False DefinitionSite -> Bool
defSiteHere Maybe DefinitionSite
mDefinitionSite
mDefSiteAnchor :: Maybe String
mDefSiteAnchor :: Maybe [Char]
mDefSiteAnchor = Maybe [Char]
-> (DefinitionSite -> Maybe [Char])
-> Maybe DefinitionSite
-> Maybe [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__ DefinitionSite -> Maybe [Char]
defSiteAnchor Maybe DefinitionSite
mDefinitionSite
link :: DefinitionSite -> Attribute
link (DefinitionSite TopLevelModuleName
m Key
defPos Bool
_here Maybe [Char]
_aName) = AttributeValue -> Attribute
Attr.href (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ [Char] -> AttributeValue
stringValue ([Char] -> AttributeValue) -> [Char] -> AttributeValue
forall a b. (a -> b) -> a -> b
$
Bool -> ShowS -> ShowS
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Key
defPos Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
<= Key
1)
([Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"#" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
ShowS
Network.URI.Encode.encode (Key -> [Char]
forall a. Show a => a -> [Char]
show Key
defPos))
(ShowS
Network.URI.Encode.encode ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> ShowS
modToFile TopLevelModuleName
m [Char]
"html")