diff --git a/src/Borceux.lagda.md b/src/Borceux.lagda.md
index 1ee1ca97b..ce229d281 100644
--- a/src/Borceux.lagda.md
+++ b/src/Borceux.lagda.md
@@ -1116,3 +1116,5 @@ _ = const-nato
* Exercise 8.4.6:
* (⇒) `dependent-product→lcc`{.Agda}
* (⇐) `lcc→dependent-product`{.Agda}
+
+[[marked graph homomorphism]]
diff --git a/support/shake/app/Definitions.hs b/support/shake/app/Definitions.hs
index 5f2c8a5a0..27f3bc1e7 100644
--- a/support/shake/app/Definitions.hs
+++ b/support/shake/app/Definitions.hs
@@ -113,7 +113,7 @@ newtype LinkTargetQ = LinkTargetQ Text
type instance RuleResult GlossaryQ = Glossary
type instance RuleResult ModuleGlossaryQ = Glossary
-type instance RuleResult LinkTargetQ = Text
+type instance RuleResult LinkTargetQ = (Text, Text)
addDefinition :: Mangled -> Definition -> Glossary -> Glossary
addDefinition _ Definition{definitionCopy = True} ge = ge
@@ -154,7 +154,7 @@ glossaryRules = do
_ <- addOracle \(LinkTargetQ target) -> do
glo <- getEntries <$> askOracle GlossaryQ
case Map.lookup (mangleLink target) glo of
- Just def -> pure $ definitionTarget def
+ Just def -> pure (definitionAnchor def, definitionTarget def)
Nothing -> error $
"Unknown wiki-link target: " ++ Text.unpack target
@@ -203,10 +203,10 @@ isWikiLink (Link attr contents (url, title))
| "wikilink" == title = pure $ WikiLink url contents attr
isWikiLink _ = Nothing
-getWikiLinkUrl :: Text -> Action Text
+getWikiLinkUrl :: Text -> Action (Text, Text)
getWikiLinkUrl = askOracle . LinkTargetQ
getWikiLink :: WikiLink -> Action Inline
-getWikiLink (WikiLink dest contents attr) = do
- url <- getWikiLinkUrl dest
- pure $ Link attr contents (url, "")
+getWikiLink (WikiLink dest contents (id, cls, kv)) = do
+ (anchor, url) <- getWikiLinkUrl dest
+ pure $ Link (id, cls, ("data-target", anchor):kv) contents (url, "")
diff --git a/support/shake/app/HTML/Backend.hs b/support/shake/app/HTML/Backend.hs
index 1ab3edca1..9c8756868 100644
--- a/support/shake/app/HTML/Backend.hs
+++ b/support/shake/app/HTML/Backend.hs
@@ -1,7 +1,9 @@
-- Copyright (c) 2005-2021 remains with the Agda authors. See /support/shake/LICENSE.agda
-- | Backend for generating highlighted, hyperlinked HTML from Agda sources.
-{-# LANGUAGE FlexibleContexts, BlockArguments, LambdaCase, DerivingStrategies, OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts, BlockArguments, LambdaCase, DerivingStrategies, OverloadedStrings, NondecreasingIndentation #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE TypeFamilies #-}
module HTML.Backend
( htmlBackend
, compileOneModule
@@ -14,56 +16,77 @@ import HTML.Base
import Prelude hiding ((!!), concatMap)
import Control.Monad.Identity
import Control.Monad.Except
+import Control.Monad.Reader
import qualified Data.HashMap.Strict as Hm
import qualified Data.Map.Strict as Map
import qualified Data.HashSet as HashSet
import qualified Data.Text as Text
+import qualified Data.Set as Set
+
import Data.HashMap.Strict (HashMap)
import Data.List.NonEmpty (NonEmpty((:|)))
import Data.Map.Strict (Map)
import Data.Foldable
import Data.HashSet (HashSet)
import Data.Aeson
+import Data.Maybe
import Data.IORef
import Data.Text (Text)
import Data.List
+import Data.Set (Set)
-import Agda.Compiler.Backend
+import Agda.Compiler.Backend hiding (topLevelModuleName)
import Agda.Compiler.Common
+import Control.DeepSeq
+
import qualified Agda.Syntax.Concrete.Generic as Con
import qualified Agda.Syntax.Internal.Generic as I
import qualified Agda.Syntax.Abstract.Views as A
+import qualified Agda.Syntax.Common.Aspect as Asp
+import qualified Agda.Syntax.Scope.Base as Scope
+import qualified Agda.Syntax.Concrete as Con
import qualified Agda.Syntax.Internal as I
import qualified Agda.Syntax.Abstract as A
-import qualified Agda.Syntax.Concrete as Con
-import qualified Agda.Syntax.Scope.Base as Scope
+import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Translation.InternalToAbstract ( Reify(reify) )
-import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)
+import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_, abstractToConcreteCtx)
import Agda.Syntax.TopLevelModuleName
+import Agda.Syntax.Abstract.Pretty (prettyA, prettyATop)
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Common.Pretty
+import Agda.Syntax.Scope.Monad (modifyCurrentScope, getCurrentModule, freshConcreteName)
import Agda.Syntax.Abstract hiding (Type)
import Agda.Syntax.Position
import Agda.Syntax.Internal (Type, domName)
+import Agda.Syntax.Fixity (Precedence(TopCtx))
import Agda.Syntax.Common
import Agda.Syntax.Info
+import qualified Agda.TypeChecking.Monad.Base as I
+import qualified Agda.TypeChecking.Pretty as P
+import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Telescope
+import Agda.TypeChecking.Records (isRecord)
import Agda.TypeChecking.Reduce (instantiateFull, reduceDefCopyTCM, normalise)
+import Agda.TypeChecking.Level (reallyUnLevelView)
+import qualified Agda.Utils.Maybe.Strict as S
import Agda.Utils.FileName
+import Agda.Utils.Lens
+import Agda.Utils.Size
import System.FilePath hiding (normalise)
-import Debug.Trace
-import qualified Agda.Utils.Maybe.Strict as S
-import Agda.Syntax.Scope.Monad (modifyCurrentScope)
-import Agda.Syntax.Abstract.Pretty (prettyA)
-import Agda.TypeChecking.Records (isRecord)
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Agda.TypeChecking.Level (reallyUnLevelView)
+
+import Text.Show.Pretty (ppShow)
+
+import HTML.Render
+import Debug.Trace (traceShow)
+import Agda.Syntax.Internal.Names (namesIn')
+import Agda.Interaction.Response (Response_boot(Resp_RunningInfo))
+import Agda.Interaction.Options.Lenses (LensVerbosity(setVerbosity))
data HtmlCompileEnv = HtmlCompileEnv
{ htmlCompileEnvOpts :: HtmlOptions
@@ -163,12 +186,13 @@ compileDefHtml env _ _ _
compileDefHtml env _menv _isMain def = withCurrentModule (qnameModule (defName def)) $
case definitionAnchor env def of
Just mn -> do
- ty <- typeToText def
+ (tooltip, ty) <- typeToText def
let
ident = Identifier
- { idAnchor = mn
- , idIdent = Text.pack (render (pretty (qnameName (defName def))))
- , idType = ty
+ { idAnchor = mn
+ , idIdent = Text.pack (render (pretty (qnameName (defName def))))
+ , idType = ty
+ , idTooltip = tooltip
}
pure (Just (mn, ident))
Nothing -> do
@@ -196,6 +220,7 @@ postModuleHtml env menv _isMain _modName _defs = do
. htmlCompileEnvOpts
. htmlModEnvCompileEnv
$ menv
+
htmlSrc <- srcFileOfInterface (htmlModEnvName menv) <$> curIF
runLogHtmlWithMonadDebug $ generatePage htmlSrc
pure $ HtmlModule $ foldr ins mempty _defs
@@ -233,23 +258,6 @@ compileOneModule _pn opts types iface = do
compDef env menv def = setCurrentRange (defName def) $
compileDefHtml env menv NotMain def
-killQual :: Con.Expr -> Con.Expr
-killQual = Con.mapExpr (wrap . forget) where
- work :: Con.QName -> Con.QName
- work (Con.Qual _ x) = work x
- work x = x
-
- forget :: Con.Expr -> Con.Expr
- forget (Con.KnownOpApp r w qual names args) = Con.OpApp w qual names args
- forget (Con.KnownIdent r nm) = Con.Ident nm
- forget x = x
-
- wrap :: Con.Expr -> Con.Expr
- wrap (Con.Ident v) = Con.Ident (work v)
- wrap (Con.KnownIdent v w) = Con.KnownIdent v (work w)
- wrap (Con.OpApp v qual names args) = Con.OpApp v (work qual) names args
- wrap x = x
-
getClass :: QName -> TCM (Set QName)
getClass q = isRecord q >>= \case
Just RecordData{ _recFields = f } -> pure $! Set.fromList (map I.unDom f)
@@ -264,43 +272,96 @@ usedInstances = I.foldTerm \case
Nothing -> pure mempty
_ -> pure mempty
-typeToText :: Definition -> TCM Text
+typeToText :: Definition -> TCM (Text, Text)
typeToText d = do
ui <- usedInstances (I.unEl (defType d))
+ fv <- getDefFreeVars (defName d)
+
ty <- locallyReduceDefs (OnlyReduceDefs ui) $ normalise (defType d)
- expr <- runNoCopy (reify ty)
- fmap (Text.pack . render . pretty . killQual) .
- abstractToConcrete_ . removeImpls $ expr
+
+ topm <- topLevelModuleName (qnameModule (defName d))
+
+ let
+ n k = Asp.Name (Just k) False
+ asp = \case
+ I.Axiom{} -> n Asp.Postulate
+ DataOrRecSig{} -> n Asp.Datatype
+ GeneralizableVar{} -> n Asp.Generalizable
+ AbstractDefn d -> asp d
+ d@Function{}
+ | isProperProjection d -> n Asp.Field
+ | otherwise -> n Asp.Function
+ Datatype{} -> n Asp.Datatype
+ Record{} -> n Asp.Record{}
+ Constructor{conSrcCon = c} ->
+ n $ Asp.Constructor (I.conInductive c)
+ I.Primitive{} -> n Asp.Primitive
+ PrimitiveSort{} -> Asp.PrimitiveType
+
+ aspect = asp (theDef d)
+
+ a = Asp.Aspects
+ { Asp.aspect = Just aspect
+ , Asp.otherAspects = mempty
+ , Asp.note = ""
+ , Asp.definitionSite = toDefinitionSite topm (nameBindingSite (qnameName (defName d)))
+ , Asp.tokenBased = Asp.TokenBased
+ }
+
+ expr <- removeImpls <$> reify ty
+
+ here <- currentTopLevelModule
+ tooltip <- fmap renderToHtml $ P.vcat
+ [ annotate a <$> P.pretty (qnameName (defName d))
+ , P.nest 2 (P.colon P.<+> prettyATop expr)
+ ]
+ plain <- Text.pack . render <$> prettyATop expr
+ pure (tooltip, plain)
+
+toDefinitionSite :: TopLevelModuleName -> Range -> Maybe Asp.DefinitionSite
+toDefinitionSite topm r = do
+ p <- fmap (fromIntegral . posPos) . rStart $ r
+ pure $ Asp.DefinitionSite
+ { Asp.defSiteModule = topm
+ , Asp.defSitePos = fromIntegral p
+ , Asp.defSiteHere = True
+ , Asp.defSiteAnchor = Nothing
+ }
+
+killQual :: Con.Expr -> Con.Expr
+killQual = Con.mapExpr wrap where
+ work :: Con.QName -> Con.QName
+ work (Con.Qual _ x) = work x
+ work x = x
+
+ wrap :: Con.Expr -> Con.Expr
+ wrap (Con.Ident v) = Con.Ident (work v)
+ wrap (Con.KnownIdent v w) = Con.KnownIdent v (work w)
+ wrap (Con.KnownOpApp v a b c d) = Con.KnownOpApp v a (work b) c d
+ wrap (Con.OpApp v qual names args) = Con.OpApp v (work qual) names args
+ wrap x = x
removeImpls :: A.Expr -> A.Expr
removeImpls (A.Pi _ (x :| xs) e) =
- makePi (map (A.mapExpr removeImpls) $ filter ((/= Hidden) . getHiding) (x:xs)) (removeImpls e)
+ let
+ fixup :: TypedBinding -> TypedBinding
+ fixup q@(TBind rng inf as _)
+ | Hidden <- getHiding q = TBind rng inf as underscore
+ | otherwise = q
+ in makePi (map (A.mapExpr removeImpls) $ map fixup (x:xs)) (removeImpls e)
removeImpls (A.Fun span arg ret) =
A.Fun span (removeImpls <$> arg) (removeImpls ret)
removeImpls e = e
makePi :: [A.TypedBinding] -> A.Expr -> A.Expr
-makePi [] = id
-makePi (b:bs) = A.Pi exprNoRange (b :| bs)
-
-newtype NoCopy a = NoCopy { runNoCopy :: TCM a }
- deriving newtype (Functor, Applicative, Monad, MonadFail)
- deriving newtype
- ( HasBuiltins, MonadDebug, MonadReduce, HasOptions, MonadTCEnv
- , ReadTCState, MonadAddContext, MonadInteractionPoints
- , MonadFresh NameId
- )
-
-noCopyOp :: Definition -> Definition
-noCopyOp def | defCopy def, Con.numHoles (defName def) >= 1 = traceShow (pretty (defName def)) $ def{defCopy = False}
-noCopyOp def = def
-
-instance HasConstInfo NoCopy where
- getConstInfo = NoCopy . fmap noCopyOp . getConstInfo
- getConstInfo' = NoCopy . fmap (fmap noCopyOp) . getConstInfo'
- getRewriteRulesFor = NoCopy . getRewriteRulesFor
-
-instance PureTCM NoCopy
+makePi [] e = e
+makePi (b:bs) (A.Pi _ bs' e') = makePi (b:bs ++ toList bs') e'
+makePi (b:bs) e = A.Pi exprNoRange (b `mergeTBinds` bs) e
+
+mergeTBinds :: A.TypedBinding -> [A.TypedBinding] -> NonEmpty A.TypedBinding
+mergeTBinds (A.TBind r i as Underscore{}) (A.TBind _ _ as' Underscore{}:bs) =
+ mergeTBinds (A.TBind r i (as <> as') underscore) bs
+mergeTBinds x xs = x :| xs
definitionAnchor :: HtmlCompileEnv -> Definition -> Maybe Text
definitionAnchor _ def | defCopy def = Nothing
diff --git a/support/shake/app/HTML/Base.hs b/support/shake/app/HTML/Base.hs
index 408fbb3ba..d2f1162b0 100644
--- a/support/shake/app/HTML/Base.hs
+++ b/support/shake/app/HTML/Base.hs
@@ -2,7 +2,7 @@
-- | Function for generating highlighted, hyperlinked HTML from Agda
-- sources.
-{-# LANGUAGE FlexibleInstances, DeriveGeneric, OverloadedStrings, DeriveAnyClass #-}
+{-# LANGUAGE FlexibleInstances, DeriveGeneric, OverloadedStrings, DeriveAnyClass, BlockArguments #-}
module HTML.Base
( HtmlOptions(..)
, defaultHtmlOptions
@@ -18,23 +18,25 @@ module HTML.Base
import Prelude hiding ((!!), concatMap)
+import Control.Monad.Trans.Reader ( ReaderT(runReaderT), ask )
+import Control.Monad.Trans ( MonadIO(..), lift )
import Control.DeepSeq
import Control.Monad
-import Control.Monad.Trans ( MonadIO(..), lift )
-import Control.Monad.Trans.Reader ( ReaderT(runReaderT), ask )
+import qualified Data.HashMap.Strict as Hm
+import qualified Data.Text.Lazy as T
+import qualified Data.HashSet as Hs
+import qualified Data.IntMap as IntMap
+import qualified Data.List as List
+import qualified Data.Text as Ts
+import Data.HashMap.Strict (HashMap)
+import Data.List.Split (splitWhen)
+import Data.Text.Lazy (Text)
import Data.Function ( on )
import Data.Foldable (toList, concatMap)
+import Data.HashSet (HashSet)
import Data.Maybe
import Data.Aeson
-import qualified Data.IntMap as IntMap
-import qualified Data.List as List
-import Data.List.Split (splitWhen)
-import Data.Text.Lazy (Text)
-import qualified Data.Text.Lazy as T
-import qualified Data.Text as Ts
-import Data.HashMap.Strict (HashMap)
-import qualified Data.HashMap.Strict as Hm
import GHC.Generics (Generic)
@@ -74,6 +76,8 @@ import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Impossible
+import HTML.Render
+
-- | Determine how to highlight the file
data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
@@ -81,15 +85,6 @@ data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
instance NFData HtmlHighlight
--- | Data about an identifier
-data Identifier = Identifier
- { idIdent :: Ts.Text
- , idAnchor :: Ts.Text
- , idType :: Ts.Text
- }
- deriving (Eq, Show, Ord, Generic, ToJSON, FromJSON, NFData)
-
-
highlightOnlyCode :: HtmlHighlight -> FileType -> Bool
highlightOnlyCode HighlightAll _ = False
highlightOnlyCode HighlightCode _ = True
@@ -168,35 +163,50 @@ renderSourceFile
:: HashMap Ts.Text Identifier
-> HtmlOptions
-> HtmlInputSourceFile
- -> Text
-renderSourceFile types opts = renderSourcePage where
- htmlHighlight = htmlOptHighlight opts
- renderSourcePage (HtmlInputSourceFile moduleName fileType sourceCode hinfo) =
- page opts onlyCode moduleName pageContents
- where
- tokens = tokenStream sourceCode hinfo
- onlyCode = highlightOnlyCode htmlHighlight fileType
- pageContents = code types onlyCode fileType tokens
+ -> (Text, [Ts.Text])
+renderSourceFile types opts (HtmlInputSourceFile moduleName fileType sourceCode hinfo) =
+ let
+ htmlHighlight = htmlOptHighlight opts
+
+ tokens = tokenStream sourceCode hinfo
+ onlyCode = highlightOnlyCode htmlHighlight fileType
+
+ used :: Int -> [TokenInfo] -> (HashMap Ts.Text (Int, Identifier), [Ts.Text])
+ used !n ((_, _, a):ts)
+ | Just ds <- definitionSite a
+ , Just id <- Hm.lookup (Ts.pack (definitionSiteToAnchor ds)) types
+ , (map, list) <- used (n + 1) ts
+ = (Hm.insert (idAnchor id) (n, id) map, idTooltip id:list)
+ | otherwise = used n ts
+ used _ [] = mempty
+
+ (order, usedts) = used 0 tokens
+ pageContents = code order onlyCode fileType moduleName tokens
+ in
+ rnf order `seq`
+ ( page opts onlyCode moduleName pageContents
+ , usedts
+ )
defaultPageGen
:: (MonadIO m, MonadLogHtml m)
=> HashMap Ts.Text Identifier
-> HtmlOptions
- -> HtmlInputSourceFile -> m ()
+ -> HtmlInputSourceFile
+ -> m ()
defaultPageGen types opts srcFile@(HtmlInputSourceFile moduleName ft _ _) = do
let
- ext = highlightedFileExt (htmlOptHighlight opts) ft
- target = htmlOptDir opts modToFile moduleName ext
- typeTarget = htmlOptDir opts modToFile moduleName "json"
- html = renderSourceFile types opts srcFile
+ ext = highlightedFileExt (htmlOptHighlight opts) ft
+ target = htmlOptDir opts modToFile moduleName ext
+ typeTarget = htmlOptDir opts modToFile moduleName "json"
+ ourTypes = htmlOptDir opts modToFile moduleName "used"
+ (html, used) = renderSourceFile types opts srcFile
logHtml $ render $ "Generating HTML for" <+> pretty moduleName
writeRenderedHtml html target
- liftIO $ encodeFile typeTarget types
-
--- | Converts module names to the corresponding HTML file names.
-modToFile :: TopLevelModuleName -> String -> FilePath
-modToFile m ext = Network.URI.Encode.encode $ render (pretty m) <.> ext
+ liftIO do
+ encodeFile typeTarget types
+ encodeFile ourTypes used
-- | Generates a highlighted, hyperlinked version of the given module.
@@ -208,11 +218,6 @@ writeRenderedHtml
writeRenderedHtml html target = liftIO $ UTF8.writeTextToFile target html
--- | Attach multiple Attributes
-
-(!!) :: Html -> [Attribute] -> Html
-h !! as = h ! mconcat as
-
-- | Constructs the web page, including headers.
page
@@ -271,12 +276,13 @@ tokenStream contents info =
-- | Constructs the HTML displaying the code.
code
- :: HashMap Ts.Text Identifier
+ :: HashMap Ts.Text (Int, Identifier)
-> Bool -- ^ Whether to generate non-code contents as-is
-> FileType -- ^ Source file type
+ -> TopLevelModuleName
-> [TokenInfo]
-> Html
-code types _onlyCode _fileType = mconcat . map mkMd . splitByMarkup
+code types _onlyCode _fileType mod = mconcat . map mkMd . splitByMarkup
where
trd (_, _, a) = a
@@ -287,7 +293,7 @@ code types _onlyCode _fileType = mconcat . map mkMd . splitByMarkup
mkHtml (pos, s, mi) =
-- Andreas, 2017-06-16, issue #2605:
-- Do not create anchors for whitespace.
- applyUnless (mi == mempty) (annotate pos mi) $ toHtml s
+ applyUnless (mi == mempty) (aspectsToHtml (Just mod) types (Just pos) mi) $ toHtml s
backgroundOrAgdaToHtml :: TokenInfo -> Html
backgroundOrAgdaToHtml token@(_, s, mi) = case aspect mi of
@@ -304,74 +310,3 @@ code types _onlyCode _fileType = mconcat . map mkMd . splitByMarkup
formatCode = Html5.pre ! Attr.class_ "Agda" $ mconcat $ backgroundOrAgdaToHtml <$> tokens
formatNonCode = mconcat $ backgroundOrAgdaToHtml <$> 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 pos mi =
- applyWhen hereAnchor (anchorage nameAttributes mempty <>) . anchorage posAttributes
- where
- -- Warp an anchor ( tag) with the given attributes around some HTML.
- anchorage :: [Attribute] -> Html -> Html
- anchorage attrs html = Html5.a html !! attrs
-
- -- File position anchor (unique, reliable).
- posAttributes :: [Attribute]
- posAttributes = concat
- [ [Attr.id $ stringValue $ show pos ]
- , concat (maybeToList (link <$> definitionSite mi))
- , Attr.class_ (stringValue $ unwords classes) <$ guard (not $ null classes)
- ]
-
- -- Named anchor (not reliable, but useful in the general case for outside refs).
- nameAttributes :: [Attribute]
- nameAttributes = [ Attr.id $ stringValue $ fromMaybe __IMPOSSIBLE__ $ mDefSiteAnchor ]
-
- classes = concat
- [ otherAspectClasses (toList $ otherAspects mi)
- , concatMap aspectClasses (aspect mi)
- ]
-
- aspectClasses (Name mKind op) = kindClass ++ opClass
- where
- kindClass = toList $ fmap showKind mKind
-
- showKind (Constructor Inductive) = "InductiveConstructor"
- showKind (Constructor CoInductive) = "CoinductiveConstructor"
- showKind k = show k
-
- opClass = ["Operator" | op]
- aspectClasses a = [show a]
-
- otherAspectClasses = map show
-
- -- 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 = here && isJust mDefSiteAnchor
-
- mDefinitionSite :: Maybe DefinitionSite
- mDefinitionSite = definitionSite mi
-
- -- Are we at the definition site now?
- here :: Bool
- here = maybe False defSiteHere mDefinitionSite
-
- mDefSiteAnchor :: Maybe String
- mDefSiteAnchor = maybe __IMPOSSIBLE__ defSiteAnchor mDefinitionSite
-
- link :: DefinitionSite -> [Attribute]
- link (DefinitionSite m defPos _here _aName) =
- [ Attr.href $ stringValue $ anchor ]
- ++ maybeToList (Html5.dataAttribute "type" . textValue . idType <$> ident_)
- where
- anchor :: String
- anchor =
- applyUnless (defPos <= 1)
- (++ "#" ++ Network.URI.Encode.encode (show defPos))
- (Network.URI.Encode.encode $ modToFile m "html")
- ident_ :: Maybe Identifier
- ident_ = Hm.lookup (Ts.pack anchor) types
diff --git a/support/shake/app/HTML/Render.hs b/support/shake/app/HTML/Render.hs
new file mode 100644
index 000000000..54cd1dacf
--- /dev/null
+++ b/support/shake/app/HTML/Render.hs
@@ -0,0 +1,171 @@
+{-# LANGUAGE DeriveGeneric, DeriveAnyClass, OverloadedStrings, BlockArguments #-}
+module HTML.Render where
+
+import Prelude hiding ((!!))
+
+import Agda.Interaction.Highlighting.Common
+
+import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
+import Agda.Syntax.Common.Aspect
+import Agda.Syntax.Common.Pretty
+
+import Agda.Utils.Impossible (__IMPOSSIBLE__)
+import Agda.Utils.Function
+
+import Control.DeepSeq
+import Control.Monad
+
+import qualified Data.HashMap.Strict as Hm
+import qualified Data.Text.Lazy as Tl
+import qualified Data.Text as Text
+import Data.HashMap.Strict (HashMap)
+import Data.Foldable
+import Data.Hashable
+import Data.Aeson
+import Data.Maybe
+import Data.Text (Text)
+
+import GHC.Generics
+
+import qualified Network.URI.Encode
+
+import System.FilePath
+
+import qualified Text.PrettyPrint.Annotated.HughesPJ as Ppr
+import qualified Text.PrettyPrint.Annotated as Ppr
+
+import qualified Text.Blaze.Html5.Attributes as Attr
+import Text.Blaze.Html.Renderer.Text ( renderHtml )
+import Text.Blaze.Html5 as Html hiding (map)
+
+data DocTree = Node Aspects [DocTree] | Text Text.Text | Mark (Maybe Aspects)
+
+renderToHtml :: Doc -> Text
+renderToHtml = finish . Ppr.fullRenderAnn Ppr.PageMode 100 1.5 cont [] where
+ consText (Ppr.Chr c) (Text t:ts) = Text (c `Text.cons` t):ts
+ consText (Ppr.Str c) (Text t:ts) = Text (Text.pack c <> t):ts
+ consText (Ppr.PStr c) (Text t:ts) = Text (Text.pack c <> t):ts
+ consText (Ppr.Chr c) ts = Text (Text.singleton c):ts
+ consText (Ppr.Str c) ts = Text (Text.pack c):ts
+ consText (Ppr.PStr c) ts = Text (Text.pack c):ts
+
+ annotate acc (Mark (Just t):ts) = Node t (reverse acc):ts
+ annotate acc (Mark Nothing:ts) = reverse acc <> ts
+ annotate acc (t:ts) = annotate (t:acc) ts
+ annotate acc [] = __IMPOSSIBLE__
+
+ cont :: Ppr.AnnotDetails Aspects -> [DocTree] -> [DocTree]
+ cont ann acc = case ann of
+ Ppr.AnnotStart -> annotate [] acc
+ Ppr.NoAnnot d _ -> consText d acc
+ Ppr.AnnotEnd a
+ | _:_ <- toAtoms a -> Mark (Just a):acc
+ | otherwise -> Mark Nothing:acc -- uncurry (<>) (break acc)
+
+ toBlaze :: DocTree -> Html
+ toBlaze (Mark _) = __IMPOSSIBLE__
+ toBlaze (Text t) = Html.text t
+ toBlaze (Node a t) = Html.span do
+ aspectsToHtml Nothing mempty Nothing a $
+ traverse_ toBlaze t
+ unless (null (note a)) do
+ Html.span (string (note a)) !! [Attr.class_ "Note"]
+
+ finish = Tl.toStrict . renderHtml . wrapper
+ wrapper = (!! [Attr.class_ "Agda"]) . Html.pre . traverse_ toBlaze
+
+-- | Data about an identifier
+data Identifier = Identifier
+ { idIdent :: Text
+ , idAnchor :: Text
+ , idType :: Text
+ , idTooltip :: Text
+ }
+ deriving (Eq, Show, Ord, Generic, ToJSON, FromJSON, NFData)
+
+instance Hashable Identifier where
+ hashWithSalt s = hashWithSalt s . idAnchor
+
+-- | Attach multiple Attributes
+(!!) :: Html -> [Attribute] -> Html
+h !! as = h ! mconcat as
+
+-- | Converts module names to the corresponding HTML file names.
+modToFile :: TopLevelModuleName -> String -> FilePath
+modToFile m ext = Network.URI.Encode.encode $ render (pretty m) <.> ext
+
+-- 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).
+aspectsToHtml :: Maybe TopLevelModuleName -> HashMap Text.Text (Int, Identifier) -> Maybe Int -> Aspects -> Html -> Html
+aspectsToHtml ourmod types pos mi =
+ applyWhen hereAnchor (anchorage nameAttributes mempty <>) . anchorage posAttributes
+ where
+ -- Warp an anchor ( tag) with the given attributes around some HTML.
+ anchorage :: [Attribute] -> Html -> Html
+ anchorage attrs html = Html.a html !! attrs
+
+ -- File position anchor (unique, reliable).
+ posAttributes :: [Attribute]
+ posAttributes = concat
+ [ [Attr.id $ stringValue $ show pos | Just pos <- [pos]]
+ , concat (maybeToList (link <$> definitionSite mi))
+ , Attr.class_ (stringValue $ unwords classes) <$ guard (not $ null classes)
+ ]
+
+ -- Named anchor (not reliable, but useful in the general case for outside refs).
+ nameAttributes :: [Attribute]
+ nameAttributes = [ Attr.id $ stringValue $ fromMaybe __IMPOSSIBLE__ $ mDefSiteAnchor ]
+
+ classes = concat
+ [ otherAspectClasses (toList $ otherAspects mi)
+ , concatMap aspectClasses (aspect mi)
+ ]
+
+ aspectClasses (Name mKind op) = kindClass ++ opClass
+ where
+ kindClass = toList $ fmap showKind mKind
+
+ showKind (Constructor Inductive) = "InductiveConstructor"
+ showKind (Constructor CoInductive) = "CoinductiveConstructor"
+ showKind k = show k
+
+ opClass = ["Operator" | op]
+ aspectClasses a = [show a]
+
+ otherAspectClasses = map show
+
+ -- 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 = here && isJust mDefSiteAnchor
+
+ mDefinitionSite :: Maybe DefinitionSite
+ mDefinitionSite = definitionSite mi
+
+ -- Are we at the definition site now?
+ here :: Bool
+ here = maybe False defSiteHere mDefinitionSite
+
+ mDefSiteAnchor :: Maybe String
+ mDefSiteAnchor = maybe __IMPOSSIBLE__ defSiteAnchor mDefinitionSite
+
+ link :: DefinitionSite -> [Html.Attribute]
+ link ds@(DefinitionSite m defPos _here _aName) =
+ let
+ anchor :: String
+ anchor = definitionSiteToAnchor ds
+
+ ident_ :: Maybe Int
+ ident_ = fst <$> Hm.lookup (Text.pack anchor) types
+ in [ Attr.href $ stringValue $ anchor ]
+ ++ maybeToList (Html.dataAttribute "module" . stringValue . show . pretty <$> ourmod)
+ ++ maybeToList (Html.dataAttribute "identifier" . stringValue . show <$> ident_)
+
+definitionSiteToAnchor :: DefinitionSite -> String
+definitionSiteToAnchor (DefinitionSite m defPos _ _) =
+ applyUnless (defPos <= 1)
+ (++ "#" ++ Network.URI.Encode.encode (show defPos))
+ (Network.URI.Encode.encode $ modToFile m "html")
diff --git a/support/shake/app/Main.hs b/support/shake/app/Main.hs
index bce65c9e5..8ceae2d33 100755
--- a/support/shake/app/Main.hs
+++ b/support/shake/app/Main.hs
@@ -82,25 +82,33 @@ rules = do
let modName = dropExtension (takeFileName out)
modKind <- Map.lookup modName <$> getOurModules
-
skipAgda <- getSkipAgda
- if skipAgda
- then
- let
- input = case modName of
+ let
+ input
+ | not skipAgda = "_build/html0" modName
+ | otherwise = case modName of
"all-pages" -> "_build/all-pages"
_ -> "src" map (\c -> if c == '.' then '/' else c) modName
- in
- case modKind of
- Just WithText -> buildMarkdown modName (input <.> ".lagda.md") out
- _ -> copyFile' (input <.> ".agda") out -- Wrong, but eh!
- else
- let input = "_build/html0" modName in
- case modKind of
- Just WithText -> do buildMarkdown modName (input <.> ".md") out
- _ -> copyFile' (input <.> ".html") out
+
+ inext = case modKind of
+ Just WithText
+ | skipAgda -> "lagda.md"
+ | otherwise -> "md"
+ _ -> if skipAgda then "agda" else "html"
+
+ case modKind of
+ Just WithText -> buildMarkdown modName (input <.> inext) out
+ _ -> copyFile' (input <.> inext) out -- Wrong, but eh!
+
+ unless skipAgda $ need ["_build/html/types" modName <.> "json"]
"_build/search/*.json" %> \out -> need ["_build/html" takeFileName out -<.> "html"]
+ "_build/html/types/*.json" %> \out -> do
+ let
+ mn = takeFileName out
+ it = "_build/html0/" mn -<.> "used"
+ need [it]
+ copyFile' it $ "_build/html/types/" mn
"_build/html/static/search.json" %> \out -> do
skipAgda <- getSkipAgda
@@ -111,12 +119,18 @@ rules = do
traced "Writing search data" $ encodeFile out (concat searchData)
-- Compile Quiver to SVG. This is used by 'buildMarkdown'.
- "_build/html/light-*.svg" %> \out -> do
- let inp = "_build/diagrams" drop (length ("light-" :: String)) (takeFileName out) -<.> "tex"
+ "_build/html/**/*.light.svg" %> \out -> do
+ let
+ inp = "_build/diagrams"
+ takeFileName (takeDirectory out)
+ takeBaseName out -<.> "tex"
buildDiagram (getPreambleFor False) inp out False
- "_build/html/dark-*.svg" %> \out -> do
- let inp = "_build/diagrams" drop (length ("dark-" :: String)) (takeFileName out) -<.> "tex"
+ "_build/html/**/*.dark.svg" %> \out -> do
+ let
+ inp = "_build/diagrams"
+ takeFileName (takeDirectory out)
+ takeBaseName out -<.> "tex"
buildDiagram (getPreambleFor True) inp out True
"_build/html/css/*.css" %> \out -> do
@@ -154,8 +168,11 @@ rules = do
need and kicks off the above job to build them.
-}
phony "all" do
- agda <- getAllModules >>= \modules ->
- pure ["_build/html" f <.> "html" | (f, _) <- Map.toList modules]
+ skipAgda <- getSkipAgda
+ agda <- getAllModules >>= \modules -> pure do
+ (f, _) <- Map.toList modules
+ [ "_build/html" f <.> "html" ] <>
+ [ "_build/html/types" f <.> "json" | not skipAgda ]
static <- getDirectoryFiles "support/static/" ["**/*"] >>= \files ->
pure ["_build/html/static" f | f <- files]
need $
diff --git a/support/shake/app/Shake/AgdaCompile.hs b/support/shake/app/Shake/AgdaCompile.hs
index 71c071b59..8fbef9e90 100644
--- a/support/shake/app/Shake/AgdaCompile.hs
+++ b/support/shake/app/Shake/AgdaCompile.hs
@@ -38,6 +38,8 @@ import Agda.Syntax.TopLevelModuleName
, hashRawTopLevelModuleName
)
import Agda.Syntax.Position (noRange)
+import qualified Agda.Utils.Maybe.Strict as S
+import qualified Agda.Utils.Trie as Trie
import Agda.Utils.FileName
import Agda.Utils.Hash (Hash)
import Agda.Utils.Lens ((^.))
@@ -119,13 +121,14 @@ agdaRules = do
-- Add a couple of forwarding rules for emitting the actual HTML/MD
"_build/html0/*.html" %> \file -> need [file -<.> "json"]
- "_build/html0/*.md" %> \file -> need [file -<.> "json"]
+ "_build/html0/*.used" %> \file -> need [file -<.> "json"]
+ "_build/html0/*.md" %> \file -> need [file -<.> "json"]
-- We generate the all-types JSON from the all-pages types JSON - it's just a
-- schema change.
"_build/all-types.json" %> \file -> do
types <- getTypes "all-pages"
- liftIO $ encodeFile file (Hm.elems types)
+ liftIO $ encodeFile file $ map (\t -> t{idTooltip = ""}) (Hm.elems types)
-- | Compile the top-level Agda file.
compileAgda :: IORef (Maybe TCState) -> Action CompileA
@@ -180,14 +183,16 @@ emitAgda
emitAgda (CompileA tcState _) getTypes modName = do
basepn <- filePath <$> liftIO (absolute "src/")
- let tlModName = toTopLevel tcState modName
- iface = getInterface tcState tlModName
+ let
+ tlModName = toTopLevel tcState modName
+ iface = getInterface tcState tlModName
types <- parallel . map (getTypes . render . pretty . fst) $ iImportedModules iface
skipTypes <- getSkipTypes
((), _) <- quietly . traced "agda html"
. runTCM initEnv tcState
+ . withScope_ (iInsideScope iface)
. locallyTC eActiveBackendName (const $ Just "HTML") $ do
compileOneModule basepn defaultHtmlOptions { htmlOptGenTypes = not skipTypes }
(mconcat types)
diff --git a/support/shake/app/Shake/KaTeX.hs b/support/shake/app/Shake/KaTeX.hs
index 2820ac0f6..a1ecd33e6 100644
--- a/support/shake/app/Shake/KaTeX.hs
+++ b/support/shake/app/Shake/KaTeX.hs
@@ -5,11 +5,14 @@ module Shake.KaTeX
( katexRules
, getDisplayMath
, getInlineMath
+ , prerenderMaths
, getParsedPreamble
, getPreambleFor
) where
+import Control.Monad
+
import qualified Data.ByteString.Lazy as LazyBS
import qualified Data.Text.Encoding as Text
import qualified Data.Text.IO as Text
@@ -44,6 +47,9 @@ getDisplayMath contents = askOracle (LatexEquation (True, contents))
getInlineMath :: Text -> Action Text
getInlineMath contents = askOracle (LatexEquation (False, contents))
+prerenderMaths :: [Text] -> [Text] -> Action ()
+prerenderMaths display inline = void . askOracles $ [LatexEquation (True, c) | c <- display] <> [LatexEquation (False, c) | c <- inline]
+
-- | Get the preamble for a given build ('True' = dark mode)
getPreambleFor :: Bool -> Action Text
getPreambleFor = askOracle . LatexPreamble
@@ -67,7 +73,7 @@ katexRules = versioned 2 do
let dark = if bool then darkSettings else mempty
pure (preambleToLatex pre <> Text.pack "\n" <> dark)
- _ <- addOracleCache \(LatexEquation (display, tex)) -> do
+ _ <- versioned 2 $ addOracleCache \(LatexEquation (display, tex)) -> do
pre <- askOracle (ParsedPreamble ())
let args = ["-T", "-F", "html"] ++ ["-d" | display]
diff --git a/support/shake/app/Shake/LinkGraph.hs b/support/shake/app/Shake/LinkGraph.hs
index cc1044efc..3cb101394 100644
--- a/support/shake/app/Shake/LinkGraph.hs
+++ b/support/shake/app/Shake/LinkGraph.hs
@@ -47,7 +47,7 @@ linksRules = do
let searchAnchors = Set.fromList (map idAnchor searchData)
agdaIdents :: [Identifier] <- readJSONFile "_build/all-types.json"
let agdaAnchors = Set.fromList [ Text.concat [filename, "#", ident]
- | Identifier ident anchor _type <- agdaIdents
+ | Identifier ident anchor _type _tooltip <- agdaIdents
, let (filename, _) = Text.break (== '#') anchor ]
pure $ Set.unions [moduleAnchors, searchAnchors, agdaAnchors]
diff --git a/support/shake/app/Shake/LinkReferences.hs b/support/shake/app/Shake/LinkReferences.hs
index a676e1029..e53c15221 100644
--- a/support/shake/app/Shake/LinkReferences.hs
+++ b/support/shake/app/Shake/LinkReferences.hs
@@ -42,12 +42,13 @@ linkReferences modname (Pandoc meta blocks) = Pandoc meta (walk link blocks)
link x = x
renderReference :: Reference -> Text -> Inline
-renderReference (Reference href cls) t =
- Span ("", ["Agda"], []) [Link ("", [cls], []) [Code nullAttr t] (href, "")]
+renderReference (Reference href cls ty) t =
+ Span ("", ["Agda"], []) [Link ("", [cls], maybeToList (("data-identifier",) <$> ty)) [Code nullAttr t] (href, "")]
data Reference =
Reference { refHref :: Text
, refClass :: Text
+ , refType :: Maybe Text
}
deriving (Eq, Show)
@@ -65,7 +66,7 @@ parseSymbolRefs = go mempty . concatMap getHTML where
go map (TagOpen "a" meta:TagText t:TagClose "a":xs)
| Just cls <- lookup "class" meta
, Just href <- lookup "href" meta
- = go (addIfNotPresent t (Reference href cls) map) xs
+ = go (addIfNotPresent t (Reference href cls (lookup "data-identifier" meta)) map) xs
| otherwise = go map xs
diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs
index 251a7f4f1..b62cb486b 100644
--- a/support/shake/app/Shake/Markdown.hs
+++ b/support/shake/app/Shake/Markdown.hs
@@ -16,6 +16,7 @@ import Control.Applicative
import qualified Data.ByteString.Lazy as LazyBS
import qualified Data.Text.Encoding as Text
import qualified Data.Map.Lazy as Map
+import qualified Data.Sequence as Seq
import qualified Data.Text.IO as Text
import qualified Data.Text as Text
import qualified Data.Set as Set
@@ -214,6 +215,7 @@ buildMarkdown modname input output = do
= Meta
. Map.insert "title" (mStr title)
. Map.insert "source" (mStr permalink)
+ . Map.insert "module" (mStr modname)
. Map.insert "bibliography" (mStr bibliographyName)
. Map.insert "link-citations" (MetaBool True)
. unMeta
@@ -224,9 +226,16 @@ buildMarkdown modname input output = do
either (fail . show) pure =<< runIO do
(,) <$> processCitations pandoc <*> getReferences Nothing pandoc
- liftIO $ Dir.createDirectoryIfMissing False "_build/diagrams"
+ liftIO $ Dir.createDirectoryIfMissing True $ "_build/diagrams" modname
- let refMap = Map.fromList $ map (\x -> (Cite.unItemId . Cite.referenceId $ x, x)) references
+ let
+ refMap = Map.fromList $ map (\x -> (Cite.unItemId . Cite.referenceId $ x, x)) references
+ (display, inline) = flip query markdown \case
+ Math DisplayMath contents -> (Seq.singleton contents, mempty)
+ Math InlineMath contents -> (mempty, Seq.singleton contents)
+ _ -> mempty
+
+ prerenderMaths (toList display) (toList inline)
Pandoc meta@(Meta metamap) blocks <-
walkM (patchInline refMap)
@@ -241,10 +250,10 @@ buildMarkdown modname input output = do
baseUrl <- getBaseUrl
- filtered <- parallel $ map (runWriterT . walkM (patchBlock baseUrl)) blocks
- let (bs, mss) = unzip filtered
- MarkdownState references = fold mss
- markdown = Pandoc meta bs
+ filtered <- parallel $ map (runWriterT . walkM (patchBlock baseUrl modname)) blocks
+ let (bs, mss) = unzip filtered
+ MarkdownState references defs = fold mss
+ markdown = Pandoc meta bs
digest <- do
cssDigest <- getFileDigest "_build/html/css/default.css"
@@ -264,10 +273,18 @@ buildMarkdown modname input output = do
traverse_ (checkMarkup input) tags
traced "writing" do
- Text.writeFile output $ renderHTML5 tags
+ Dir.createDirectoryIfMissing False "_build/html/fragments"
Dir.createDirectoryIfMissing False "_build/search"
+
+ Text.writeFile output $ renderHTML5 tags
encodeFile ("_build/search" modname <.> "json") search
+ for_ (Map.toList defs) \(key, bs) -> traced "writing fragment" do
+ text <- either (fail . show) pure =<<
+ runIO (renderMarkdown authors references modname baseUrl digest (Pandoc mempty bs))
+
+ Text.writeFile ("_build/html/fragments" Text.unpack (getMangled key) <.> "html") text
+
-- | Find the original Agda file from a 1Lab module name.
findModule :: MonadIO m => String -> m FilePath
findModule modname = do
@@ -322,10 +339,18 @@ patchInline _ (Str s)
patchInline _ h = pure h
-newtype MarkdownState = MarkdownState
- { mdReferences :: [Val Text] -- ^ List of references extracted from Pandoc's "reference" div.
+data MarkdownState = MarkdownState
+ { mdReferences :: [Val Text]
+ -- ^ List of references extracted from Pandoc's "reference" div.
+ , mdDefinitions :: Map.Map Mangled [Block]
+ -- ^ List of definition blocks
}
- deriving newtype (Semigroup, Monoid)
+
+instance Semigroup MarkdownState where
+ MarkdownState a b <> MarkdownState a' b' = MarkdownState (a <> a') (b <> b')
+
+instance Monoid MarkdownState where
+ mempty = MarkdownState mempty mempty
diagramResource :: Resource
diagramResource = unsafePerformIO $ newResourceIO "diagram" 1
@@ -335,22 +360,23 @@ diagramResource = unsafePerformIO $ newResourceIO "diagram" 1
patchBlock
:: (MonadIO f, MonadFail f, MonadWriter MarkdownState f, MonadTrans t, f ~ t Action)
=> String
+ -> String
-> Block
-> f Block
-- Make all headers links, and add an anchor emoji.
-patchBlock _ (Header i a@(ident, _, _) inl) = pure $ Header i a
+patchBlock _ _ (Header i a@(ident, _, _) inl) = pure $ Header i a
$ htmlInl (Text.concat [""]
-- Replace quiver code blocks with a link to an SVG file, and depend on the SVG file.
-patchBlock _ (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` classes = do
+patchBlock _ mod (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` classes = do
let
- digest = showDigest . sha1 . LazyBS.fromStrict $ Text.encodeUtf8 contents
+ digest = take 12 . showDigest . sha1 . LazyBS.fromStrict $ Text.encodeUtf8 contents
title = fromMaybe "commutative diagram" (lookup "title" attrs)
- light = "_build/html/light-" <> digest <.> "svg"
- dark = "_build/html/dark-" <> digest <.> "svg"
+ lfn = mod digest <.> "light.svg"
+ dfn = mod digest <.> "dark.svg"
height <- lift do
-- We have to lock the diagram directory to prevent race conditions
@@ -359,25 +385,25 @@ patchBlock _ (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` classes
-- This isn't the best in terms of atomicity, but it does preserve
-- the nice property that diagrams are globally shared by their
-- contents.
- withResource diagramResource 1 $ liftIO $
- Text.writeFile ("_build/diagrams" digest <.> "tex") contents
+ withResource diagramResource 1 $ liftIO do
+ Text.writeFile ("_build/diagrams" mod digest <.> "tex") contents
- need [ light, dark ]
- diagramHeight light
+ need [ "_build/html" lfn, "_build/html" dfn ]
+ diagramHeight ("_build/html" lfn)
let attrs' = ("style", "--height: " <> Text.pack (show height) <> "px;"):attrs
pure $ Div ("", ["diagram-container"], [])
- [ Plain [ Image (id, "diagram diagram-light":classes, attrs') [] (Text.pack ("light-" <> digest <.> "svg"), title) ]
- , Plain [ Image (id, "diagram diagram-dark":classes, attrs') [] (Text.pack ("dark-" <> digest <.> "svg"), title) ]
+ [ Plain [ Image (id, "diagram diagram-light":classes, attrs') [] (Text.pack lfn, title) ]
+ , Plain [ Image (id, "diagram diagram-dark":classes, attrs') [] (Text.pack dfn, title) ]
]
-patchBlock base (Div attr@("recent-additions", _, _) []) =
+patchBlock base _ (Div attr@("recent-additions", _, _) []) =
Div attr . map (renderCommit base) <$> lift recentAdditions
-- Find the references block, parse the references, and remove it. We write
-- the references as part of our template instead.
-patchBlock _ (Div ("refs", _, _) body) = do
+patchBlock _ _ (Div ("refs", _, _) body) = do
for_ body \ref -> case ref of
(Div (id, _, _) body) -> do
-- If our citation is a single paragraph, don't wrap it in .
@@ -397,7 +423,13 @@ patchBlock _ (Div ("refs", _, _) body) = do
_ -> fail ("Unknown reference node " ++ show ref)
pure $ Plain [] -- TODO: pandoc-types 1.23 removed Null
-patchBlock _ h = pure h
+patchBlock _ _ b@(Div (id, [only], kv) bs) | "definition" == only, not (Text.null id) = do
+ let
+ isfn (Note _) = True
+ isfn _ = False
+ b <$ tell (MarkdownState mempty (Map.singleton (mangleLink id) (walk (filter (not . isfn)) bs)))
+
+patchBlock _ _ h = pure h
-- | Render our Pandoc document using the given template variables.
renderMarkdown
@@ -414,12 +446,15 @@ renderMarkdown authors references modname baseUrl digest markdown@(Pandoc (Meta
isTalk = isJust $ Map.lookup "talk" meta
templateName
- | isTalk = talkTemplateName
- | otherwise = pageTemplateName
+ | isTalk = Just talkTemplateName
+ | mempty == meta = Nothing
+ | otherwise = Just pageTemplateName
+
+ get nm = getTemplate nm
+ >>= runWithPartials . compileTemplate nm
+ >>= either (throwError . PandocTemplateError . Text.pack) pure
- template <- getTemplate templateName
- >>= runWithPartials . compileTemplate templateName
- >>= either (throwError . PandocTemplateError . Text.pack) pure
+ template <- traverse get templateName
let
authors' = case authors of
@@ -436,7 +471,7 @@ renderMarkdown authors references modname baseUrl digest markdown@(Pandoc (Meta
]
opts = def
- { writerTemplate = Just template
+ { writerTemplate = template
, writerTableOfContents = not isTalk
, writerVariables = context
, writerExtensions = getDefaultExtensions "html"
diff --git a/support/web/css/code.scss b/support/web/css/code.scss
index 8b85703ad..3549710e5 100644
--- a/support/web/css/code.scss
+++ b/support/web/css/code.scss
@@ -167,19 +167,3 @@ code.at, span.at { color: theme(--code-constructor); } /* Attribute */
code.do, span.do { color: theme(--code-string); } /* Documentation */
code.an, span.an { color: theme(--code-string); } /* Annotation */
code.cv, span.cv { color: theme(--code-string); } /* CommentVar */
-
-.type-tooltip, div.sourceCode.type-tooltip {
- position: absolute;
- z-index: 100;
-
- font-size: 0.8em;
- color: theme(--code-fg);
- background: theme(--code-bg);
-
- &.sourceCode {
- padding: 0.3em;
- border: 0;
- };
-
- box-shadow: 2px 2px 6px theme(--shadow);
-}
diff --git a/support/web/css/components/popup.scss b/support/web/css/components/popup.scss
new file mode 100644
index 000000000..ea29e1b2d
--- /dev/null
+++ b/support/web/css/components/popup.scss
@@ -0,0 +1,65 @@
+div.hover-popup, div.hover-popup.sourceCode {
+ &.popup-hidden { display: none; }
+ @include widescreen { display: block; }
+
+ position: absolute;
+ z-index: 100;
+
+ color: theme(--code-fg);
+ background: theme(--code-bg);
+
+ --font-size: 1.125rem;
+ --code-font-size: 1rem;
+
+ box-shadow: 2px 2px 6px theme(--shadow);
+
+ >:first-child { margin-block-start: 0; }
+ >:last-child { margin-block-end: 0; }
+
+ padding: 0.3em;
+ border: 0;
+ margin: 0;
+
+ &:before {
+ display: none;
+ }
+}
+
+.text-popup {
+ min-width: 22em;
+ max-width: 26em;
+ width: min-content;
+
+ margin-left: 1.25em;
+}
+
+
+@mixin keyframes-for($dir, $dy) {
+ @keyframes popup-fade-in-#{$dir} {
+ 0% {
+ opacity: 0;
+ transform: translate(0, $dy);
+ }
+ 100% {
+ opacity: 1;
+ transform: translate(0, 0);
+ }
+ }
+
+ @keyframes popup-fade-out-#{$dir} {
+ 0% {
+ opacity: 1;
+ transform: translate(0, 0);
+ }
+ 100% {
+ opacity: 0;
+ transform: translate(0, $dy);
+ }
+ }
+
+ .popup-fade-in-#{$dir} { animation: 0.3s popup-fade-in-#{$dir}; }
+ .popup-fade-out-#{$dir} { animation: 0.3s popup-fade-out-#{$dir}; }
+}
+
+@include keyframes-for(up, 10px);
+@include keyframes-for(down, -10px);
diff --git a/support/web/css/default.scss b/support/web/css/default.scss
index f5a5e29e3..3a0089226 100644
--- a/support/web/css/default.scss
+++ b/support/web/css/default.scss
@@ -8,6 +8,7 @@
@import "components/commit.scss";
@import "components/search.scss";
@import "components/modal.scss";
+@import "components/popup.scss";
@import "components/toc.scss";
@import "code.scss";
@@ -25,10 +26,12 @@ html, body, main, div#post-toc-container {
max-width: 100vw;
}
-body {
+body, p {
font-family: var(--serif), var(--sans-serif);
font-size: var(--font-size);
+}
+body {
width: 100%;
&.text-page {
@@ -264,7 +267,11 @@ div.diagram-container {
}
}
-main a[href], div#return > a[href], div#top > a[href], aside#toc > div#toc-container ul a[href] {
+main a[href],
+div#return > a[href],
+div#top > a[href],
+aside#toc > div#toc-container ul a[href],
+div.hover-popup a[href] {
color: theme(--primary);
text-decoration: none;
diff --git a/support/web/css/mixins.scss b/support/web/css/mixins.scss
index a6228eb1e..4e80017d6 100644
--- a/support/web/css/mixins.scss
+++ b/support/web/css/mixins.scss
@@ -19,6 +19,15 @@
left: calc(-1 * #{$left-border-distance} - #{$left-border-width});
}
}
+
+ @at-root div.hover-popup & {
+ border-inline-start: 0;
+ padding-inline-start: 0;
+
+ &:before {
+ display: none;
+ }
+ }
}
@mixin material($bg) {
diff --git a/support/web/js/highlight-hover.ts b/support/web/js/highlight-hover.ts
index 88a2926db..7e406a7ee 100644
--- a/support/web/js/highlight-hover.ts
+++ b/support/web/js/highlight-hover.ts
@@ -2,12 +2,77 @@
// https://github.com/haskell/haddock/blob/ghc-8.8/LICENSE
// Slightly modified by Tesla Ice Zhang
-let links: Array = [];
+import { Hover } from './lib/hover';
-let currentHover: HTMLDivElement | null = null;
+let links: Array = [];
+const paths: { module: string, baseURL: string, source: string } = window as any;
const page = window.location.pathname.slice(1).replace(".html", "");
+const types: Map> = new Map();
+
+/**
+ * Fetch the types of identifiers used in a given module.
+ *
+ * @param mod The module
+ * @returns
+ * A promise resolving to the types of every identifier used in that
+ * module, in some arbitrary order.
+ */
+async function fetchTypes(mod: string): Promise {
+ if (types.get(mod)) return types.get(mod)!;
+
+ const prommy = fetch(`${paths.baseURL}/types/${mod}.json`, { method: 'get' }).then(async (r) => {
+ if (!r.ok) throw `Failed to load type-on-hover information for module ${paths.module}`;
+ return await r.json() as string[];
+ });
+
+ types.set(mod, prommy);
+ return prommy;
+}
+
+/**
+ * Construct a Hover appropriate for the given link element, fetching
+ * the appropriate content.
+ *
+ * @param a The element
+ * @returns The instantiated hover, or undefined if this element has no associated popup.
+ */
+function getHover(a: HTMLAnchorElement): Hover | undefined {
+ let target;
+ if (Hover.get(a)) return Hover.get(a);
+
+ if (!Number.isNaN(target = Number.parseInt(a.getAttribute("data-identifier") ?? ""))) {
+ let tgt = target;
+ const mod = a.getAttribute("data-module") ?? paths.module;
+
+ const get = fetchTypes(mod).then((tys) => {
+ const element = document.createElement("div");
+ element.innerHTML = tys[tgt]!;
+ element.classList.add("hover-popup", "sourceCode");
+
+ return element;
+ });
+
+ return new Hover(a, get, true);
+ } else if ((target = a.getAttribute("data-target")) != null) {
+ const tgt = target;
+ const get = fetch(`${paths.baseURL}/fragments/${tgt}.html`, { method: 'get' }).then(async (p) => {
+ if (!p.ok) throw `Failed to load fragment ${tgt}`;
+
+ const element = document.createElement("div");
+ element.innerHTML = await p.text();
+ element.classList.add("hover-popup", "text-popup");
+
+ return element;
+ });
+
+ return new Hover(a, get, false);
+ }
+
+ return;
+}
+
/* A `highlight` event contains:
* `link`: HTMLAnchorElement | Node
* either a link or a node in the dependency graph
@@ -19,36 +84,19 @@ document.addEventListener('highlight', (({ detail: { link, on } }: CustomEvent)
let match: (a : HTMLAnchorElement) => boolean;
if (link instanceof HTMLAnchorElement) {
- const type = link.getAttribute("data-type");
- if (type) {
- if (currentHover) {
- currentHover.remove();
- currentHover = null;
- }
-
- if (on) {
- currentHover = document.createElement("div");
- currentHover.innerText = type;
- currentHover.classList.add("type-tooltip", "sourceCode");
- document.body.appendChild(currentHover);
-
- const selfRect = link.getBoundingClientRect();
- const hoverRect = currentHover.getBoundingClientRect();
-
- console.log(link.getClientRects())
+ match = that => that.href === link.href;
- // If we're close to the bottom of the page, push the tooltip above instead.
- // The constant here is arbitrary, because trying to convert em to px in JS is a fool's errand.
- if (selfRect.bottom + hoverRect.height + 30 > window.innerHeight) {
- // 2em from the material mixin. I'm sorry
- currentHover.style.top = `calc(${selfRect.top - hoverRect.height}px - 1em`;
- } else {
- currentHover.style.top = `${selfRect.top + (selfRect.height / 2)}px`;
+ requestAnimationFrame(async () => {
+ try {
+ const hover = await getHover(link);
+ if (hover) {
+ await hover.mouseEvent(on);
}
- currentHover.style.left = `${selfRect.left}px`;
+ } catch (e) {
+ console.log(e);
}
- }
- match = that => that.href === link.href;
+ });
+
} else {
// Don't light up the entire page when hovering over the central node.
if (link.id === page)
@@ -59,24 +107,27 @@ document.addEventListener('highlight', (({ detail: { link, on } }: CustomEvent)
links.forEach(that => {
if (match(that)) {
- if (on)
- that.classList.add("hover-highlight");
- else
- that.classList.remove("hover-highlight");
+ that.classList.toggle("hover-highlight", on);
}
});
}) as EventListener);
-export function refreshLinks() {
- links = Array.from(document.getElementsByTagName("a"));
- links.forEach(link => {
- if (link.hasAttribute("href")) {
- link.onmouseover = () => document.dispatchEvent(new CustomEvent('highlight', { detail: { link, on: true } }))
- link.onmouseout = () => document.dispatchEvent(new CustomEvent('highlight', { detail: { link, on: false } }))
- }
+export function refreshLinks(parent?: HTMLElement): HTMLAnchorElement[] {
+ if (!parent) links = [];
+
+ const here = Array.from((parent ?? document.documentElement).querySelectorAll("a[href]")) as HTMLAnchorElement[];
+ links.push(...here);
+
+ here.forEach(link => {
+ link.addEventListener("mouseenter", () =>
+ document.dispatchEvent(new CustomEvent('highlight', { detail: { link, on: true } })));
+ link.addEventListener("mouseleave", () =>
+ document.dispatchEvent(new CustomEvent('highlight', { detail: { link, on: false } })));
});
+
+ return here;
}
-document.addEventListener("DOMContentLoaded", refreshLinks);
+document.addEventListener("DOMContentLoaded", () => refreshLinks());
export {};
diff --git a/support/web/js/lib/hover.ts b/support/web/js/lib/hover.ts
new file mode 100644
index 000000000..4e2a6f858
--- /dev/null
+++ b/support/web/js/lib/hover.ts
@@ -0,0 +1,251 @@
+import { refreshLinks } from "../highlight-hover";
+import { Timeout } from "./timeout";
+
+const showTimeout: number = 250;
+const hideTimeout: number = 500;
+const
+ currentHovers: Map = new Map(),
+ hovers: Map = new Map();
+
+export class Hover {
+ /* To put ourselves in the `hovers` map, we need to be able to refer to
+ * hovers by something that's not the element, since, in the
+ * constructor, the element may not exist yet. */
+ private static nextHover = 0;
+
+ /** How many cursors are currently over this hover? */
+ private cursors: number = 0;
+
+ /** Function to be invoked when this popup disappears. Also serves as a
+ * proxy for whether or not we've drawn it.
+ * */
+ private shown?: () => void;
+
+ /** If this popup is associated to an element in another popup, this
+ * stores that other popup. */
+ private parent?: Hover;
+
+ /** Stores any of the children of this popup that have been rendered.
+ * The promise resolves when that child closes. */
+ private children: Map> = new Map();
+
+ /**
+ * Constructs the hover, and sets up the popup element.
+ *
+ * @param anchor The link to which we belong.
+ * @param element A promise that will resolve with the popup container.
+ * @param ephemeral
+ * Whether this popup should fade in/out, and also whether it
+ * should be shared.
+ */
+ constructor(private anchor: HTMLElement, private element: Promise, private ephemeral: boolean) {
+ currentHovers.set(anchor, this);
+
+ // We figure out parents by id because we don't yet have the element
+ // here.
+ const
+ myself = `hover-popup-${++Hover.nextHover}`,
+ parent = anchor.closest("div.hover-popup");
+
+ hovers.set(myself, this);
+ if (parent && hovers.get(parent.id)) this.parent = hovers.get(parent.id);
+
+ element.then((e) => {
+ e.classList.add('popup-hidden');
+ e.id = myself;
+
+ e.addEventListener("mouseenter", async () => this.fading || await this.mouseEvent(true));
+ e.addEventListener("mouseleave", async () => this.fading || await this.mouseEvent(false));
+
+ refreshLinks(e);
+
+ document.body.appendChild(e);
+ });
+ }
+
+ private fadeDirection?: 'up' | 'down';
+
+ /**
+ * Show the popup and decide on the positioning, hence in which
+ * direction the popup will fade.
+ */
+ private async place() {
+ const el = await this.element;
+ if (this.cursors <= 0 || this.shown) return;
+
+ el.classList.remove('popup-hidden');
+
+ const selfRect = this.anchor.getBoundingClientRect();
+ const hoverRect = el.getBoundingClientRect();
+
+ if (selfRect.bottom + hoverRect.height + 48 > window.innerHeight) {
+ // Tooltip placed above anchor
+ el.style.top = `calc(${window.scrollY + selfRect.top - hoverRect.height}px - 1.3rem)`;
+ this.fadeDirection = 'down';
+ } else {
+ // Tooltip placed below anchor
+ el.style.top = `${window.scrollY + selfRect.bottom}px`;
+ this.fadeDirection = 'up';
+ }
+
+ if (selfRect.left + hoverRect.width > window.innerWidth) {
+ el.style.left = `calc(${selfRect.right - hoverRect.width}px)`;
+ } else {
+ el.style.left = `${selfRect.left}px`;
+ }
+
+ if (!this.ephemeral) {
+ el.classList.remove(`popup-fade-out-${this.fadeDirection}`);
+ el.classList.add(`popup-fade-in-${this.fadeDirection}`);
+ }
+
+ // Instead of having a boolean to indicate what's been shown, we use
+ // the closing signal as a sentinel instead.
+ this.shown = this.blockParent();
+ }
+
+ /**
+ * Add this element to the map of its parents' children, and update
+ * the closing promise.
+ *
+ * @returns
+ * A function that, when invoked, signals to the parent that
+ * this child has closed.
+ */
+ private blockParent(): () => void {
+ if (!this.parent) return () => { };
+
+ let resolve: () => void;
+ this.parent.children.set(this, new Promise((res) => {
+ resolve = res
+ }));
+
+ return () => {
+ this.parent?.children.delete(this);
+ requestAnimationFrame(resolve!);
+ }
+ }
+
+ /** Are we playing the closing animation? */
+ private closing?: Timeout;
+
+ /**
+ * Hide the popup. Does not remove the element from the DOM!
+ */
+ private async displace() {
+ const el = await this.element;
+
+ // Set ourselves to a hiding state immediately, so that if the user
+ // goes back onto the link while we're closing we can just
+ // immediately show again.
+ if (this.shown) this.shown();
+ delete this.shown;
+
+ if (!this.ephemeral) {
+ el.classList.remove(`popup-fade-in-${this.fadeDirection}`);
+ el.classList.add(`popup-fade-out-${this.fadeDirection}`);
+ }
+
+ this.closing = new Timeout(this.ephemeral ? 0 : 250, `displace ${this.anchor}`);
+
+ await this.closing.start();
+ el.classList.add('popup-hidden')
+
+ delete this.closing;
+
+ if (this.ephemeral) return this.destroy();
+ }
+
+ private async destroy() {
+ const el = await this.element;
+ el.remove();
+
+ currentHovers.delete(this.anchor);
+ hovers.delete(el.id);
+ }
+
+ /** Are we closing this popup, or does it associated with an anchor
+ * that belongs to a parent which is fading? */
+ private get fading(): boolean {
+ return !!this.closing || (!!this.parent && this.parent.fading)
+ }
+
+ /** Timeout before the popup appears. */
+ private showTimer?: Timeout;
+
+ /**
+ * Handle an update when the popup is not shown yet. Depending on
+ * whether or not the cursor is over this popup (or its anchor),
+ * either show it, or cancel a previous show timer if one exists..
+ */
+ private async unhide() {
+ if (this.cursors >= 1) {
+ this.showTimer = new Timeout(this.ephemeral ? 0 : showTimeout, `unhide ${this.anchor}`);
+
+ // If we're currently playing the closing animation, but there's a
+ // positive number of cursors (necessarily on the anchor), then we
+ // should wait and show the popup again.
+ try {
+ if (this.closing) await this.closing.start();
+
+ await Promise.all([this.showTimer?.start(), this.element]);
+ await this.place();
+
+ delete this.showTimer;
+ } catch (e) {
+ if (e === this.showTimer?.cancelled) return;
+ throw e;
+ }
+ } else if (this.cursors <= 0 && this.showTimer && !this.showTimer.done) {
+ this.showTimer?.cancel();
+ if (this.ephemeral) this.destroy();
+ }
+ }
+
+
+ private hideTimer?: Timeout;
+
+ /**
+ * Handle an update when the popup has been shown. Depending on
+ * whether the cursor is over this popup (or its anchor), either
+ * hide/destroy it, or cancel a previous unshowing.
+ */
+ private async unshow() {
+ if (this.cursors <= 0) {
+ this.hideTimer = new Timeout(this.ephemeral ? 0 : hideTimeout, `unshow ${this.anchor}`);
+
+ try {
+ await Promise.all(Array.from(this.children.values()).concat(this.hideTimer.start()));
+
+ if (this.cursors > 0) return;
+ await this.displace();
+
+ } catch (e) {
+ if (e == this.hideTimer.cancelled) return;
+ throw e;
+ }
+ } else if (this.cursors >= 1 && this.hideTimer && !this.hideTimer.done) {
+ this.hideTimer?.cancel();
+ }
+ }
+
+ /**
+ * Handle the mouse entering/leaving either the popup or its anchor
+ * element.
+ *
+ * @param on Did the mouse move onto the popup, or off it?
+ */
+ public async mouseEvent(on: boolean) {
+ this.cursors = Math.max(this.cursors + (on ? 1 : -1), 0);
+
+ if (!this.shown) {
+ await this.unhide();
+ } else {
+ await this.unshow();
+ }
+ }
+
+ public static get(a: HTMLElement): Hover | undefined {
+ return currentHovers.get(a)
+ }
+};
diff --git a/support/web/js/lib/timeout.ts b/support/web/js/lib/timeout.ts
new file mode 100644
index 000000000..d62fb36d7
--- /dev/null
+++ b/support/web/js/lib/timeout.ts
@@ -0,0 +1,38 @@
+class TimeoutCancelled { constructor(public name: string) { } };
+
+export class Timeout {
+ public cancelled: TimeoutCancelled;
+
+ private token?: number;
+ private reject?: (t: TimeoutCancelled) => void;
+ public done: boolean = false;
+
+ constructor(private duration: number, public name: string) {
+ this.cancelled = new TimeoutCancelled(name);
+ }
+
+ private promise?: Promise
+ public start(): Promise {
+ if (this.duration === 0) {
+ return new Promise((resolve) => resolve());
+ }
+
+ if (this.promise) return this.promise;
+
+ return this.promise = new Promise((resolve, reject) => {
+ this.token = setTimeout(() => {
+ this.done = true;
+ resolve();
+ }, this.duration);
+ this.reject = reject;
+ })
+ }
+
+ public cancel() {
+ if (this.done)
+ throw "Attempted to cancel a timeout that finished"
+
+ clearTimeout(this.token)
+ if (this.reject) this.reject(this.cancelled);
+ }
+}
diff --git a/support/web/template.html b/support/web/template.html
index 465e738ac..4ffa2d1d5 100644
--- a/support/web/template.html
+++ b/support/web/template.html
@@ -30,6 +30,14 @@
$endif$
+
+
@@ -51,13 +59,6 @@
-
-