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

module Agda.Interaction.Highlighting.HTML
  ( generateHTML
  -- Reused by PandocAgda
  , defaultCSSFile
  , generateHTMLWithPageGen
  , generatePage
  , page
  , tokenStream
  , code
  ) where

import Prelude hiding ((!!), concatMap)
import Control.Monad
import Control.Monad.Trans

import Data.Function
import Data.Foldable (toList, concatMap)
import Data.Maybe
import qualified Data.IntMap as IntMap
import qualified Data.Map    as Map
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 qualified Network.URI.Encode

import System.FilePath
import System.Directory

import Text.Blaze.Html5 hiding (code, map, title)
import qualified Text.Blaze.Html5 as Html5
import Text.Blaze.Html5.Attributes as Attr
import Text.Blaze.Html.Renderer.Text
  -- 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.Options
import Agda.Interaction.Highlighting.Precise

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

import Agda.TypeChecking.Monad (TCM, useTC)
import qualified Agda.TypeChecking.Monad as TCM

import Agda.Utils.FileName (filePath)
import Agda.Utils.Function
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- | The name of the default CSS file.

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

-- | The directive inserted before the rendered code blocks

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

-- | Determine how to highlight the file

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"

-- | Generates HTML files from all the sources which have been
--   visited during the type checking phase.
--
--   This function should only be called after type checking has
--   completed successfully.

type PageGen = FilePath    -- ^ Output directory
  -> FileType              -- ^ Source file type
  -> Bool                  -- ^ Return value of `highlightOnlyCode`
  -> String                -- ^ Output file extension (return
                           --   value of `highlightedFileExt`)
  -> C.TopLevelModuleName
  -> Text
  -> CompressedFile        -- ^ Highlighting information
  -> TCM ()

generateHTML :: TCM ()
generateHTML :: TCM ()
generateHTML = PageGen -> TCM ()
generateHTMLWithPageGen PageGen
pageGen
  where
  pageGen :: PageGen
  pageGen :: PageGen
pageGen FilePath
dir FileType
ft Bool
pc FilePath
ext TopLevelModuleName
mod Text
contents CompressedFile
hinfo =
    (FilePath -> FilePath -> Text)
-> FilePath -> FilePath -> TopLevelModuleName -> TCM ()
generatePage (Bool -> FileType -> FilePath -> FilePath -> Text
renderer Bool
pc FileType
ft) FilePath
ext FilePath
dir TopLevelModuleName
mod
    where
    renderer :: Bool -> FileType -> FilePath -> FilePath -> Text
    renderer :: Bool -> FileType -> FilePath -> FilePath -> Text
renderer Bool
onlyCode FileType
fileType FilePath
css FilePath
_ =
      FilePath -> Bool -> TopLevelModuleName -> Html -> Text
page FilePath
css Bool
onlyCode TopLevelModuleName
mod (Html -> Text) -> Html -> Text
forall a b. (a -> b) -> a -> b
$
      Bool -> FileType -> [TokenInfo] -> Html
code Bool
onlyCode FileType
fileType ([TokenInfo] -> Html) -> [TokenInfo] -> Html
forall a b. (a -> b) -> a -> b
$
      Text -> CompressedFile -> [TokenInfo]
tokenStream Text
contents CompressedFile
hinfo

-- | Prepare information for HTML page generation.
--
--   The page generator receives the output directory as well as the
--   module's top level module name, its source code, and its
--   highlighting information.

generateHTMLWithPageGen
  :: PageGen
     -- ^ Page generator.
  -> TCM ()
generateHTMLWithPageGen :: PageGen -> TCM ()
generateHTMLWithPageGen PageGen
generatePage = do
      CommandLineOptions
options <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
TCM.commandLineOptions

      -- There is a default directory given by 'defaultHTMLDir'
      let dir :: FilePath
dir = CommandLineOptions -> FilePath
optHTMLDir CommandLineOptions
options
      let htmlHighlight :: HtmlHighlight
htmlHighlight = CommandLineOptions -> HtmlHighlight
optHTMLHighlight CommandLineOptions
options
      IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True FilePath
dir

      -- If the default CSS file should be used, then it is copied to
      -- the output directory.
      IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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
$ CommandLineOptions -> Maybe FilePath
optCSSFile CommandLineOptions
options) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath
cssFile <- FilePath -> IO FilePath
getDataFileName FilePath
defaultCSSFile
        FilePath -> FilePath -> IO ()
copyFile FilePath
cssFile (FilePath
dir FilePath -> FilePath -> FilePath
</> FilePath
defaultCSSFile)

      FilePath -> VerboseLevel -> [FilePath] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
FilePath -> VerboseLevel -> a -> m ()
TCM.reportS FilePath
"html" VerboseLevel
1
        [ FilePath
"" :: String
        , FilePath
"Warning: HTML is currently generated for ALL files which can be"
        , FilePath
"reached from the given module, including library files."
        ]

      -- Pull source code and highlighting info from the state and
      -- generate all the web pages.
      ((TopLevelModuleName, ModuleInfo) -> TCM ())
-> [(TopLevelModuleName, ModuleInfo)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(TopLevelModuleName
n, ModuleInfo
mi) ->
              let i :: Interface
i  = ModuleInfo -> Interface
TCM.miInterface ModuleInfo
mi
                  ft :: FileType
ft = Interface -> FileType
TCM.iFileType Interface
i in
              PageGen
generatePage FilePath
dir FileType
ft
                (HtmlHighlight -> FileType -> Bool
highlightOnlyCode HtmlHighlight
htmlHighlight FileType
ft)
                (HtmlHighlight -> FileType -> FilePath
highlightedFileExt HtmlHighlight
htmlHighlight FileType
ft) TopLevelModuleName
n
                (Interface -> Text
TCM.iSource Interface
i) (Interface -> CompressedFile
TCM.iHighlighting Interface
i)) ([(TopLevelModuleName, ModuleInfo)] -> TCM ())
-> (Map TopLevelModuleName ModuleInfo
    -> [(TopLevelModuleName, ModuleInfo)])
-> Map TopLevelModuleName ModuleInfo
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Map TopLevelModuleName ModuleInfo
-> [(TopLevelModuleName, ModuleInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map TopLevelModuleName ModuleInfo -> TCM ())
-> TCMT IO (Map TopLevelModuleName ModuleInfo) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Map TopLevelModuleName ModuleInfo)
TCM.getVisitedModules

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

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

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

generatePage
  :: (FilePath -> FilePath -> Text)  -- ^ Page renderer.
  -> String                          -- ^ Output file extension.
  -> FilePath                        -- ^ Directory in which to create
                                     --   files.
  -> C.TopLevelModuleName            -- ^ Module to be highlighted.
  -> TCM ()
generatePage :: (FilePath -> FilePath -> Text)
-> FilePath -> FilePath -> TopLevelModuleName -> TCM ()
generatePage FilePath -> FilePath -> Text
renderPage FilePath
ext FilePath
dir TopLevelModuleName
mod = do
  AbsolutePath
f   <- AbsolutePath -> Maybe AbsolutePath -> AbsolutePath
forall a. a -> Maybe a -> a
fromMaybe AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe AbsolutePath -> AbsolutePath)
-> (Map TopLevelModuleName AbsolutePath -> Maybe AbsolutePath)
-> Map TopLevelModuleName AbsolutePath
-> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName
-> Map TopLevelModuleName AbsolutePath -> Maybe AbsolutePath
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
mod (Map TopLevelModuleName AbsolutePath -> AbsolutePath)
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
-> TCMT IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map TopLevelModuleName AbsolutePath) TCState
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
TCM.stModuleToSource
  FilePath
css <- FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
defaultCSSFile (Maybe FilePath -> FilePath)
-> (CommandLineOptions -> Maybe FilePath)
-> CommandLineOptions
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> Maybe FilePath
optCSSFile (CommandLineOptions -> FilePath)
-> TCMT IO CommandLineOptions -> TCMT IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
TCM.commandLineOptions
  let target :: FilePath
target = FilePath
dir FilePath -> FilePath -> FilePath
</> TopLevelModuleName -> FilePath -> FilePath
modToFile TopLevelModuleName
mod FilePath
ext
  let html :: Text
html = FilePath -> FilePath -> Text
renderPage FilePath
css (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> FilePath
filePath AbsolutePath
f
  FilePath -> VerboseLevel -> FilePath -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
FilePath -> VerboseLevel -> FilePath -> m ()
TCM.reportSLn FilePath
"html" VerboseLevel
1 (FilePath -> TCM ()) -> FilePath -> TCM ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Generating HTML for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                           Doc -> FilePath
render (TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
mod) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                           FilePath
" (" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
target FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
")."
  IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
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                  -- ^ Whether to reserve literate
     -> C.TopLevelModuleName  -- ^ Module to be highlighted.
     -> Html
     -> Text
page :: FilePath -> Bool -> TopLevelModuleName -> Html -> Text
page FilePath
css 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
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
meta Html -> [Attribute] -> Html
!! [ AttributeValue -> Attribute
charset AttributeValue
"utf-8" ]
      , Html -> Html
Html5.title (FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml (FilePath -> Html) -> FilePath -> Html
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
render (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
modName)
      , Html
link Html -> [Attribute] -> Html
!! [ AttributeValue -> Attribute
rel AttributeValue
"stylesheet"
                , AttributeValue -> Attribute
href (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue FilePath
css
                ]
      ]

    rest :: Html
rest = Html -> Html
body (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ (Html -> Html
pre (Html -> Html) -> Attribute -> Html -> Html
forall h. Attributable h => h -> Attribute -> h
! AttributeValue -> Attribute
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.
     -> CompressedFile -- ^ Highlighting information.
     -> [TokenInfo]
tokenStream :: Text -> CompressedFile -> [TokenInfo]
tokenStream Text
contents CompressedFile
info =
  ([(Maybe Aspects, (VerboseLevel, Char))] -> TokenInfo)
-> [[(Maybe Aspects, (VerboseLevel, Char))]] -> [TokenInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\[(Maybe Aspects, (VerboseLevel, Char))]
cs -> case [(Maybe Aspects, (VerboseLevel, Char))]
cs of
          (Maybe Aspects
mi, (VerboseLevel
pos, Char
_)) : [(Maybe Aspects, (VerboseLevel, Char))]
_ ->
            (VerboseLevel
pos, ((Maybe Aspects, (VerboseLevel, Char)) -> Char)
-> [(Maybe Aspects, (VerboseLevel, Char))] -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseLevel, Char) -> Char
forall a b. (a, b) -> b
snd ((VerboseLevel, Char) -> Char)
-> ((Maybe Aspects, (VerboseLevel, Char)) -> (VerboseLevel, Char))
-> (Maybe Aspects, (VerboseLevel, Char))
-> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Aspects, (VerboseLevel, Char)) -> (VerboseLevel, Char)
forall a b. (a, b) -> b
snd) [(Maybe Aspects, (VerboseLevel, 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, (VerboseLevel, Char))]] -> [TokenInfo])
-> [[(Maybe Aspects, (VerboseLevel, Char))]] -> [TokenInfo]
forall a b. (a -> b) -> a -> b
$
  ((Maybe Aspects, (VerboseLevel, Char))
 -> (Maybe Aspects, (VerboseLevel, Char)) -> Bool)
-> [(Maybe Aspects, (VerboseLevel, Char))]
-> [[(Maybe Aspects, (VerboseLevel, 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, (VerboseLevel, Char)) -> Maybe Aspects)
-> (Maybe Aspects, (VerboseLevel, Char))
-> (Maybe Aspects, (VerboseLevel, Char))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Maybe Aspects, (VerboseLevel, Char)) -> Maybe Aspects
forall a b. (a, b) -> a
fst) ([(Maybe Aspects, (VerboseLevel, Char))]
 -> [[(Maybe Aspects, (VerboseLevel, Char))]])
-> [(Maybe Aspects, (VerboseLevel, Char))]
-> [[(Maybe Aspects, (VerboseLevel, Char))]]
forall a b. (a -> b) -> a -> b
$
  ((VerboseLevel, Char) -> (Maybe Aspects, (VerboseLevel, Char)))
-> [(VerboseLevel, Char)]
-> [(Maybe Aspects, (VerboseLevel, Char))]
forall a b. (a -> b) -> [a] -> [b]
map (\(VerboseLevel
pos, Char
c) -> (VerboseLevel -> IntMap Aspects -> Maybe Aspects
forall a. VerboseLevel -> IntMap a -> Maybe a
IntMap.lookup VerboseLevel
pos IntMap Aspects
infoMap, (VerboseLevel
pos, Char
c))) ([(VerboseLevel, Char)] -> [(Maybe Aspects, (VerboseLevel, Char))])
-> [(VerboseLevel, Char)]
-> [(Maybe Aspects, (VerboseLevel, Char))]
forall a b. (a -> b) -> a -> b
$
  [VerboseLevel] -> FilePath -> [(VerboseLevel, Char)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
1..] (Text -> FilePath
T.unpack Text
contents)
  where
  infoMap :: IntMap Aspects
infoMap = File -> IntMap Aspects
toMap (CompressedFile -> File
decompress CompressedFile
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
. VerboseLevel -> [[TokenInfo]] -> [[[TokenInfo]]]
forall e. VerboseLevel -> [e] -> [[e]]
chunksOf VerboseLevel
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
. VerboseLevel -> [[TokenInfo]] -> [[[TokenInfo]]]
forall e. VerboseLevel -> [e] -> [[e]]
chunksOf VerboseLevel
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 (VerboseLevel
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) (VerboseLevel -> Aspects -> Html -> Html
annotate VerboseLevel
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@(VerboseLevel
_, 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@(VerboseLevel
_, 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
pre (Html -> Html) -> Attribute -> Html -> Html
forall h. Attributable h => h -> Attribute -> h
! AttributeValue -> Attribute
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 = [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) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
go
    where
      go :: TokenInfo -> Html
go token :: TokenInfo
token@(VerboseLevel
_, 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 :: VerboseLevel -> Aspects -> Html -> Html
annotate VerboseLevel
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
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
$ VerboseLevel -> FilePath
forall a. Show a => a -> FilePath
show VerboseLevel
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)
-> Maybe DefinitionSite -> Maybe Attribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinitionSite -> Attribute
link (Maybe DefinitionSite -> Maybe Attribute)
-> Maybe DefinitionSite -> Maybe Attribute
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi
      , AttributeValue -> Attribute
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
      [ (FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FilePath -> [FilePath]
forall p a. p -> [a]
noteClasses (Aspects -> Maybe 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 = if Bool
op then [FilePath
"Operator"] else []
    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 VerboseLevel
pos Bool
_here Maybe FilePath
_aName) = AttributeValue -> Attribute
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 -> (FilePath -> FilePath) -> FilePath -> FilePath
forall a. Bool -> (a -> a) -> a -> a
applyUnless (VerboseLevel
pos VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
1)
        (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"#" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
         FilePath -> FilePath
Network.URI.Encode.encode (VerboseLevel -> FilePath
forall a. Show a => a -> FilePath
show VerboseLevel
pos))
         -- Network.URI.Encode.encode (fromMaybe (show pos) aName)) -- Named links disabled
        (FilePath -> FilePath
Network.URI.Encode.encode (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FilePath -> FilePath
modToFile TopLevelModuleName
m FilePath
"html")