-- | Function for generating highlighted, hyperlinked HTML from Agda
-- sources.

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 qualified Data.List   as List
import Data.List.Split (splitWhen, chunksOf)
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 )
  -- The imported operator (!) attaches an Attribute to an Html value
  -- The defined operator (!!) attaches a list of such Attributes

import Paths_Agda

import Agda.Interaction.Highlighting.Precise hiding (toList)

import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Common

import qualified Agda.TypeChecking.Monad as TCM
  ( Interface(..)
  )

import Agda.Utils.Function
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- | The Agda data directory containing the files for the HTML backend.

htmlDataDir :: FilePath
htmlDataDir :: FilePath
htmlDataDir = FilePath
"html"

-- | The name of the default CSS file.

defaultCSSFile :: FilePath
defaultCSSFile :: FilePath
defaultCSSFile = FilePath
"Agda.css"

-- | The name of the occurrence-highlighting JS file.

occurrenceHighlightJsFile :: FilePath
occurrenceHighlightJsFile :: FilePath
occurrenceHighlightJsFile = FilePath
"highlight-hover.js"

-- | The directive inserted before the rendered code blocks

rstDelimiter :: String
rstDelimiter :: FilePath
rstDelimiter = FilePath
".. raw:: html\n"

-- | The directive inserted before rendered code blocks in org

orgDelimiterStart :: String
orgDelimiterStart :: FilePath
orgDelimiterStart = FilePath
"#+BEGIN_EXPORT html\n<pre class=\"Agda\">\n"

-- | The directive inserted after rendered code blocks in org

orgDelimiterEnd :: String
orgDelimiterEnd :: FilePath
orgDelimiterEnd = FilePath
"</pre>\n#+END_EXPORT\n"

-- | Determine how to highlight the file

data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
  deriving (Int -> HtmlHighlight -> ShowS
[HtmlHighlight] -> ShowS
HtmlHighlight -> FilePath
(Int -> HtmlHighlight -> ShowS)
-> (HtmlHighlight -> FilePath)
-> ([HtmlHighlight] -> ShowS)
-> Show HtmlHighlight
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [HtmlHighlight] -> ShowS
$cshowList :: [HtmlHighlight] -> ShowS
show :: HtmlHighlight -> FilePath
$cshow :: HtmlHighlight -> FilePath
showsPrec :: Int -> HtmlHighlight -> ShowS
$cshowsPrec :: Int -> HtmlHighlight -> ShowS
Show, HtmlHighlight -> HtmlHighlight -> Bool
(HtmlHighlight -> HtmlHighlight -> Bool)
-> (HtmlHighlight -> HtmlHighlight -> Bool) -> Eq HtmlHighlight
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HtmlHighlight -> HtmlHighlight -> Bool
$c/= :: HtmlHighlight -> HtmlHighlight -> Bool
== :: HtmlHighlight -> HtmlHighlight -> Bool
$c== :: 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
$cto :: forall x. Rep HtmlHighlight x -> HtmlHighlight
$cfrom :: forall x. HtmlHighlight -> Rep HtmlHighlight x
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
TexFileType  = Bool
False

-- | Determine the generated file extension

highlightedFileExt :: HtmlHighlight -> FileType -> String
highlightedFileExt :: HtmlHighlight -> FileType -> FilePath
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 = FilePath
"html"
  | Bool
otherwise = case FileType
ft of
      FileType
AgdaFileType -> FilePath
"html"
      FileType
MdFileType   -> FilePath
"md"
      FileType
RstFileType  -> FilePath
"rst"
      FileType
TexFileType  -> FilePath
"tex"
      FileType
OrgFileType  -> FilePath
"org"

-- | Options for HTML generation

data HtmlOptions = HtmlOptions
  { HtmlOptions -> FilePath
htmlOptDir                  :: FilePath
  , HtmlOptions -> HtmlHighlight
htmlOptHighlight            :: HtmlHighlight
  , HtmlOptions -> Bool
htmlOptHighlightOccurrences :: Bool
  , HtmlOptions -> Maybe FilePath
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
/= :: HtmlOptions -> HtmlOptions -> Bool
$c/= :: HtmlOptions -> HtmlOptions -> Bool
== :: HtmlOptions -> HtmlOptions -> Bool
$c== :: HtmlOptions -> HtmlOptions -> Bool
Eq

-- | Internal type bundling the information related to a module source file

data HtmlInputSourceFile = HtmlInputSourceFile
  { HtmlInputSourceFile -> TopLevelModuleName
_srcFileModuleName :: C.TopLevelModuleName
  , HtmlInputSourceFile -> FileType
_srcFileType :: FileType
  -- ^ Source file type
  , HtmlInputSourceFile -> Text
_srcFileText :: Text
  -- ^ Source text
  , HtmlInputSourceFile -> HighlightingInfo
_srcFileHighlightInfo :: HighlightingInfo
  -- ^ Highlighting info
  }

-- | Bundle up the highlighting info for a source file

srcFileOfInterface :: C.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)

-- | Logging during HTML generation

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 FilePath
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 (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 FilePath
message

runLogHtmlWith :: Monad m => HtmlLogAction m -> LogHtmlT m a -> m a
runLogHtmlWith :: 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 :: FilePath
cssFile = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
defaultCSSFile (HtmlOptions -> Maybe FilePath
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) =
    FilePath -> Bool -> Bool -> TopLevelModuleName -> Html -> Text
page FilePath
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 :: 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 -> FilePath
render (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ Doc
"Generating HTML for"  Doc -> Doc -> Doc
<+> TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
moduleName Doc -> Doc -> Doc
<+> ((Doc -> Doc
parens (FilePath -> Doc
forall a. Pretty a => a -> Doc
pretty FilePath
target)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".")
  Text -> HtmlLogAction m
forall (m :: * -> *). MonadIO m => Text -> FilePath -> m ()
writeRenderedHtml Text
html FilePath
target
  where
    ext :: FilePath
ext = HtmlHighlight -> FileType -> FilePath
highlightedFileExt (HtmlOptions -> HtmlHighlight
htmlOptHighlight HtmlOptions
opts) FileType
ft
    target :: FilePath
target = (HtmlOptions -> FilePath
htmlOptDir HtmlOptions
opts) FilePath -> ShowS
</> TopLevelModuleName -> ShowS
modToFile TopLevelModuleName
moduleName FilePath
ext
    html :: Text
html = HtmlOptions -> HtmlInputSourceFile -> Text
renderSourceFile HtmlOptions
opts HtmlInputSourceFile
srcFile

prepareCommonDestinationAssets :: MonadIO m => HtmlOptions -> m ()
prepareCommonDestinationAssets :: HtmlOptions -> m ()
prepareCommonDestinationAssets HtmlOptions
options = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  -- There is a default directory given by 'defaultHTMLDir'
  let htmlDir :: FilePath
htmlDir = HtmlOptions -> FilePath
htmlOptDir HtmlOptions
options
  Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True FilePath
htmlDir

  -- If the default CSS file should be used, then it is copied to
  -- the output directory.
  let cssFile :: Maybe FilePath
cssFile = HtmlOptions -> Maybe FilePath
htmlOptCssFile HtmlOptions
options
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe FilePath -> Bool) -> Maybe FilePath -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe FilePath
cssFile) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath
defCssFile <- FilePath -> IO FilePath
getDataFileName (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$
      FilePath
htmlDataDir FilePath -> ShowS
</> FilePath
defaultCSSFile
    FilePath -> FilePath -> IO ()
copyFile FilePath
defCssFile (FilePath
htmlDir FilePath -> ShowS
</> FilePath
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
    FilePath
highlightJsFile <- FilePath -> IO FilePath
getDataFileName (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$
      FilePath
htmlDataDir FilePath -> ShowS
</> FilePath
occurrenceHighlightJsFile
    FilePath -> FilePath -> IO ()
copyFile FilePath
highlightJsFile (FilePath
htmlDir FilePath -> ShowS
</> FilePath
occurrenceHighlightJsFile)

-- | Converts module names to the corresponding HTML file names.

modToFile :: C.TopLevelModuleName -> String -> FilePath
modToFile :: TopLevelModuleName -> ShowS
modToFile TopLevelModuleName
m FilePath
ext = ShowS
Network.URI.Encode.encode ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
render (TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
m) FilePath -> ShowS
<.> FilePath
ext

-- | Generates a highlighted, hyperlinked version of the given module.

writeRenderedHtml
  :: MonadIO m
  => Text       -- ^ Rendered page
  -> FilePath   -- ^ Output path.
  -> m ()
writeRenderedHtml :: Text -> FilePath -> m ()
writeRenderedHtml Text
html FilePath
target = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Text -> IO ()
UTF8.writeTextToFile FilePath
target Text
html


-- | Attach multiple Attributes

(!!) :: 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

-- | Constructs the web page, including headers.

page :: FilePath              -- ^ URL to the CSS file.
     -> Bool                  -- ^ Highlight occurrences
     -> Bool                  -- ^ Whether to reserve literate
     -> C.TopLevelModuleName  -- ^ Module to be highlighted.
     -> Html
     -> Text
page :: FilePath -> Bool -> Bool -> TopLevelModuleName -> Html -> Text
page FilePath
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 (FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml (FilePath -> Html) -> (Doc -> FilePath) -> Doc -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> FilePath
render (Doc -> Html) -> Doc -> Html
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
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
$ FilePath -> AttributeValue
stringValue FilePath
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
$ FilePath -> AttributeValue
stringValue FilePath
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

-- | Position, Contents, Infomation

type TokenInfo =
  ( Int
  , String
  , Aspects
  )

-- | Constructs token stream ready to print.

tokenStream
     :: Text             -- ^ The contents of the module.
     -> HighlightingInfo -- ^ Highlighting information.
     -> [TokenInfo]
tokenStream :: Text -> HighlightingInfo -> [TokenInfo]
tokenStream Text
contents HighlightingInfo
info =
  ([(Maybe Aspects, (Int, Char))] -> TokenInfo)
-> [[(Maybe Aspects, (Int, Char))]] -> [TokenInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\[(Maybe Aspects, (Int, Char))]
cs -> case [(Maybe Aspects, (Int, Char))]
cs of
          (Maybe Aspects
mi, (Int
pos, Char
_)) : [(Maybe Aspects, (Int, Char))]
_ ->
            (Int
pos, ((Maybe Aspects, (Int, Char)) -> Char)
-> [(Maybe Aspects, (Int, Char))] -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Char) -> Char
forall a b. (a, b) -> b
snd ((Int, Char) -> Char)
-> ((Maybe Aspects, (Int, Char)) -> (Int, Char))
-> (Maybe Aspects, (Int, Char))
-> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Aspects, (Int, Char)) -> (Int, Char)
forall a b. (a, b) -> b
snd) [(Maybe Aspects, (Int, Char))]
cs, Aspects -> Maybe Aspects -> Aspects
forall a. a -> Maybe a -> a
fromMaybe Aspects
forall a. Monoid a => a
mempty Maybe Aspects
mi)
          [] -> TokenInfo
forall a. HasCallStack => a
__IMPOSSIBLE__) ([[(Maybe Aspects, (Int, Char))]] -> [TokenInfo])
-> [[(Maybe Aspects, (Int, Char))]] -> [TokenInfo]
forall a b. (a -> b) -> a -> b
$
  ((Maybe Aspects, (Int, Char))
 -> (Maybe Aspects, (Int, Char)) -> Bool)
-> [(Maybe Aspects, (Int, Char))]
-> [[(Maybe Aspects, (Int, Char))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (Maybe Aspects -> Maybe Aspects -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Maybe Aspects -> Maybe Aspects -> Bool)
-> ((Maybe Aspects, (Int, Char)) -> Maybe Aspects)
-> (Maybe Aspects, (Int, Char))
-> (Maybe Aspects, (Int, Char))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Maybe Aspects, (Int, Char)) -> Maybe Aspects
forall a b. (a, b) -> a
fst) ([(Maybe Aspects, (Int, Char))]
 -> [[(Maybe Aspects, (Int, Char))]])
-> [(Maybe Aspects, (Int, Char))]
-> [[(Maybe Aspects, (Int, Char))]]
forall a b. (a -> b) -> a -> b
$
  (Int -> Char -> (Maybe Aspects, (Int, Char)))
-> [Int] -> FilePath -> [(Maybe Aspects, (Int, Char))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
pos Char
c -> (Int -> IntMap Aspects -> Maybe Aspects
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
pos IntMap Aspects
infoMap, (Int
pos, Char
c))) [Int
1..] (Text -> FilePath
T.unpack Text
contents)
  where
  infoMap :: IntMap Aspects
infoMap = HighlightingInfo -> IntMap Aspects
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap HighlightingInfo
info

-- | Constructs the HTML displaying the code.

code :: Bool     -- ^ Whether to generate non-code contents as-is
     -> FileType -- ^ Source file type
     -> [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
         -- Explicitly written all cases, so people
         -- get compile error when adding new file types
         -- when they forget to modify the code here
         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
. Int -> [[TokenInfo]] -> [[[TokenInfo]]]
forall e. Int -> [e] -> [[e]]
chunksOf Int
2 ([[TokenInfo]] -> [[[TokenInfo]]])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [[[TokenInfo]]]
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
         -- Any points for using this option?
         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
. Int -> [[TokenInfo]] -> [[[TokenInfo]]]
forall e. Int -> [e] -> [[e]]
chunksOf Int
2 ([[TokenInfo]] -> [[[TokenInfo]]])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [[[TokenInfo]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
         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
  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 (Int
pos, FilePath
s, Aspects
mi) =
    -- Andreas, 2017-06-16, issue #2605:
    -- Do not create anchors for whitespace.
    Bool -> (Html -> Html) -> Html -> Html
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Aspects
mi Aspects -> Aspects -> Bool
forall a. Eq a => a -> a -> Bool
== Aspects
forall a. Monoid a => a
mempty) (Int -> Aspects -> Html -> Html
annotate Int
pos Aspects
mi) (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml FilePath
s

  -- Proposed in #3373, implemented in #3384
  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
. (FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml FilePath
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
go
    where
      go :: TokenInfo -> Html
go token :: TokenInfo
token@(Int
_, FilePath
s, Aspects
mi) = if Aspects -> Maybe Aspect
aspect Aspects
mi Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Background
        then FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
s
        else TokenInfo -> Html
mkHtml TokenInfo
token

  -- Proposed in #3137, implemented in #3313
  -- Improvement proposed in #3366, implemented in #3367
  mkMd :: [[TokenInfo]] -> Html
  mkMd :: [[TokenInfo]] -> Html
mkMd = [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
. [[TokenInfo]] -> [Html]
go
    where
      work :: TokenInfo -> Html
work token :: TokenInfo
token@(Int
_, FilePath
s, Aspects
mi) = case Aspects -> Maybe Aspect
aspect Aspects
mi of
        Just Aspect
Background -> FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
s
        Just Aspect
Markup     -> Html
forall a. HasCallStack => a
__IMPOSSIBLE__
        Maybe Aspect
_               -> TokenInfo -> Html
mkHtml TokenInfo
token
      go :: [[TokenInfo]] -> [Html]
go [[TokenInfo]
a, [TokenInfo]
b] = [ [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$ TokenInfo -> Html
work (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
a
                  , 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
work (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
b
                  ]
      go [[TokenInfo]
a]    = TokenInfo -> Html
work (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
a
      go [[TokenInfo]]
_      = [Html]
forall a. HasCallStack => a
__IMPOSSIBLE__

  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 = FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
orgDelimiterStart
      endDelimiter :: Html
endDelimiter = FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
orgDelimiterEnd

      formatCode :: [Html]
formatCode = Html
startDelimiter Html -> [Html] -> [Html]
forall a. a -> [a] -> [a]
: (TokenInfo -> [Html] -> [Html]) -> [Html] -> [TokenInfo] -> [Html]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\TokenInfo
x -> (TokenInfo -> Html
go 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
go [TokenInfo]
tokens

      go :: TokenInfo -> Html
go token :: TokenInfo
token@(Int
_, FilePath
s, Aspects
mi) = if Aspects -> Maybe Aspect
aspect Aspects
mi Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Background
        then FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
s
        else TokenInfo -> Html
mkHtml TokenInfo
token

  -- Put anchors that enable referencing that token.
  -- We put a fail safe numeric anchor (file position) for internal references
  -- (issue #2756), as well as a heuristic name anchor for external references
  -- (issue #2604).
  annotate :: Int -> Aspects -> Html -> Html
  annotate :: Int -> Aspects -> Html -> Html
annotate Int
pos Aspects
mi =
    Bool -> (Html -> Html) -> Html -> Html
forall a. Bool -> (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
    -- Warp an anchor (<A> tag) with the given attributes around some HTML.
    anchorage :: [Attribute] -> Html -> Html
    anchorage :: [Attribute] -> Html -> Html
anchorage [Attribute]
attrs Html
html = Html -> Html
Html5.a Html
html Html -> [Attribute] -> Html
!! [Attribute]
attrs

    -- File position anchor (unique, reliable).
    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
$ FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
pos ]
      , Maybe Attribute -> [Attribute]
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_ (FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath]
classes) Attribute -> [()] -> [Attribute]
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
$ [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
classes)
      ]

    -- Named anchor (not reliable, but useful in the general case for outside refs).
    nameAttributes :: [Attribute]
    nameAttributes :: [Attribute]
nameAttributes = [ AttributeValue -> Attribute
Attr.id (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Maybe FilePath
mDefSiteAnchor ]

    classes :: [FilePath]
classes = [[FilePath]] -> [FilePath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ (Char -> [FilePath]) -> FilePath -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [FilePath]
forall p a. p -> [a]
noteClasses (Aspects -> FilePath
note Aspects
mi)
      , [OtherAspect] -> [FilePath]
otherAspectClasses (Set OtherAspect -> [OtherAspect]
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 -> [FilePath]) -> Maybe Aspect -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Aspect -> [FilePath]
aspectClasses (Aspects -> Maybe Aspect
aspect Aspects
mi)
      ]

    aspectClasses :: Aspect -> [FilePath]
aspectClasses (Name Maybe NameKind
mKind Bool
op) = [FilePath]
kindClass [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
opClass
      where
      kindClass :: [FilePath]
kindClass = Maybe FilePath -> [FilePath]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Maybe FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (NameKind -> FilePath) -> Maybe NameKind -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameKind -> FilePath
showKind Maybe NameKind
mKind

      showKind :: NameKind -> FilePath
showKind (Constructor Induction
Inductive)   = FilePath
"InductiveConstructor"
      showKind (Constructor Induction
CoInductive) = FilePath
"CoinductiveConstructor"
      showKind NameKind
k                         = NameKind -> FilePath
forall a. Show a => a -> FilePath
show NameKind
k

      opClass :: [FilePath]
opClass = [FilePath
"Operator" | Bool
op]
    aspectClasses Aspect
a = [Aspect -> FilePath
forall a. Show a => a -> FilePath
show Aspect
a]


    otherAspectClasses :: [OtherAspect] -> [FilePath]
otherAspectClasses = (OtherAspect -> FilePath) -> [OtherAspect] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> FilePath
forall a. Show a => a -> FilePath
show

    -- Notes are not included.
    noteClasses :: p -> [a]
noteClasses p
_s = []

    -- Should we output a named anchor?
    -- Only if we are at the definition site now (@here@)
    -- and such a pretty named anchor exists (see 'defSiteAnchor').
    hereAnchor      :: Bool
    hereAnchor :: Bool
hereAnchor      = Bool
here Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
mDefSiteAnchor

    mDefinitionSite :: Maybe DefinitionSite
    mDefinitionSite :: Maybe DefinitionSite
mDefinitionSite = Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi

    -- Are we at the definition site now?
    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 FilePath
mDefSiteAnchor  = Maybe FilePath
-> (DefinitionSite -> Maybe FilePath)
-> Maybe DefinitionSite
-> Maybe FilePath
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe FilePath
forall a. HasCallStack => a
__IMPOSSIBLE__ DefinitionSite -> Maybe FilePath
defSiteAnchor Maybe DefinitionSite
mDefinitionSite

    link :: DefinitionSite -> Attribute
link (DefinitionSite TopLevelModuleName
m Int
defPos Bool
_here Maybe FilePath
_aName) = AttributeValue -> Attribute
Attr.href (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$
      -- If the definition site points to the top of a file,
      -- we drop the anchor part and just link to the file.
      Bool -> ShowS -> ShowS
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Int
defPos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1)
        (FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"#" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++
         ShowS
Network.URI.Encode.encode (Int -> FilePath
forall a. Show a => a -> FilePath
show Int
defPos))
         -- Network.URI.Encode.encode (fromMaybe (show defPos) aName)) -- Named links disabled
        (ShowS
Network.URI.Encode.encode ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> ShowS
modToFile TopLevelModuleName
m FilePath
"html")