    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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.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 )
      -- The imported operator (!) attaches an Attribute to an Html value
      -- The defined operator (!!) attaches a list of such Attributes

    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.Setup ( getDataFileName )

    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

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

    htmlDataDir :: FilePath
    htmlDataDir :: [Char]
    htmlDataDir = [Char]
    "html"

    -- | The name of the default CSS file.

    defaultCSSFile :: FilePath
    defaultCSSFile :: [Char]
    defaultCSSFile = [Char]
    "Agda.css"

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

    occurrenceHighlightJsFile :: FilePath
    occurrenceHighlightJsFile :: [Char]
    occurrenceHighlightJsFile = [Char]
    "highlight-hover.js"

    -- | The directive inserted before the rendered code blocks

    rstDelimiter :: String
    rstDelimiter :: [Char]
    rstDelimiter = [Char]
    ".. raw:: html\n"

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

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

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

    orgDelimiterEnd :: String
    orgDelimiterEnd :: [Char]
    orgDelimiterEnd = [Char]
    "</pre>\n#+END_EXPORT\n"

    -- | Determine how to highlight the file

    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
    TreeFileType  = Bool
    True
    highlightOnlyCode HtmlHighlight
    HighlightAuto FileType
    TexFileType   = Bool
    False

    -- | Determine the generated file extension

    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"
          FileType
    TreeFileType  -> [Char]
    "tree"

    -- | Options for HTML generation

    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

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

    data HtmlInputSourceFile = HtmlInputSourceFile
      { HtmlInputSourceFile -> TopLevelModuleName
    _srcFileModuleName :: 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 ::
      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 [Char]
    message = do
        doLog <- ReaderT (HtmlLogAction m) m (HtmlLogAction m)
    forall (m :: * -> *) r. Monad m => ReaderT r m r
    ask
        lift $ doLog 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
      -- There is a default directory given by 'defaultHTMLDir'
      let htmlDir :: [Char]
    htmlDir = HtmlOptions -> [Char]
    htmlOptDir HtmlOptions
    options
      Bool -> [Char] -> IO ()
    createDirectoryIfMissing Bool
    True [Char]
    htmlDir

      -- If the default CSS file should be used, then it is copied to
      -- the output directory.
      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
        defCssFile <- [Char] -> IO [Char]
    getDataFileName ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    htmlDataDir [Char] -> ShowS
    </> [Char]
    defaultCSSFile
        copyFile defCssFile (htmlDir </> 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
        highlightJsFile <- [Char] -> IO [Char]
    getDataFileName ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    htmlDataDir [Char] -> ShowS
    </> [Char]
    occurrenceHighlightJsFile
        copyFile highlightJsFile (htmlDir </> occurrenceHighlightJsFile)

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

    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

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

    writeRenderedHtml
      :: MonadIO m
      => Text       -- ^ Rendered page
      -> FilePath   -- ^ Output path.
      -> 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

    -- | 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
         -> TopLevelModuleName    -- ^ Module to be highlighted.
         -> 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

    -- | Position, Contents, Infomation

    type TokenInfo =
      ( Int
      , String1
      , 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 =
      (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

    -- | 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
    . [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
    TreeFileType  -> ([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
             -- Two useless cases, probably will never used by anyone
             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) =
        -- Andreas, 2017-06-16, issue #2605:
        -- Do not create anchors for whitespace.
        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

      -- 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
    . ([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

      -- The assumption here and in mkOrg is that Background tokens and Agda tokens are always
      -- separated by Markup tokens, so these runs only contain one kind.
      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

      -- 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 :: 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
        -- 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
    $ [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)
          ]

        -- 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
    $ [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

        -- 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 [Char] -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe [Char]
    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 [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
    $
          -- 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 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))
             -- 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 [Char]
    "html")