fix fucked nested hovers

support/shake/app/HTML/Backend.hs

@@ -278,28 +278,27 @@ typeToText d = do
   fv <- getDefFreeVars (defName d)
 
   ty <- locallyReduceDefs (OnlyReduceDefs ui) $ normalise (defType d)
-  TelV ctx ty <- telViewUpTo fv ty
 
   topm <- topLevelModuleName (qnameModule (defName d))
 
   let
-    n s k = (s, Asp.Name (Just k) False)
+    n k = Asp.Name (Just k) False
     asp = \case
-      I.Axiom{}          -> n "postulate" Asp.Postulate
-      DataOrRecSig{}     -> n "postulate" Asp.Datatype
-      GeneralizableVar{} -> n "variable" Asp.Generalizable
+      I.Axiom{}          -> n Asp.Postulate
+      DataOrRecSig{}     -> n Asp.Datatype
+      GeneralizableVar{} -> n Asp.Generalizable
       AbstractDefn d     -> asp d
       d@Function{}
-        | isProperProjection d -> n "record field" Asp.Field
-        | otherwise -> n "function" Asp.Function
-      Datatype{}         -> n "data type" Asp.Datatype
-      Record{}           -> n "record type" Asp.Record{}
+        | isProperProjection d -> n Asp.Field
+        | otherwise -> n Asp.Function
+      Datatype{}         -> n Asp.Datatype
+      Record{}           -> n Asp.Record{}
       Constructor{conSrcCon = c} ->
-        n "constructor" $ Asp.Constructor (I.conInductive c)
-      I.Primitive{} -> n "primitive" Asp.Primitive
-      PrimitiveSort{} -> ("primitive", Asp.PrimitiveType)
+        n $ Asp.Constructor (I.conInductive c)
+      I.Primitive{} -> n Asp.Primitive
+      PrimitiveSort{} -> Asp.PrimitiveType
 
-    (kind, aspect) = asp (theDef d)
+    aspect = asp (theDef d)
 
     a = Asp.Aspects
       { Asp.aspect         = Just aspect
@@ -309,23 +308,11 @@ typeToText d = do
       , Asp.tokenBased     = Asp.TokenBased
       }
 
-    a' = Asp.Aspects
-      { Asp.aspect         = Just (Asp.Name (Just Asp.Module) False)
-      , Asp.otherAspects   = mempty
-      , Asp.note           = ""
-      , Asp.definitionSite = toDefinitionSite topm (posToRange (startPos Nothing) (startPos Nothing))
-      , Asp.tokenBased     = Asp.TokenBased
-      }
-
-    topm' = pure (hlKeyword "module") P.<+> annotate a' <$> P.pretty topm
-
-  addContext ctx do
-  expr <- reify ty
+  expr <- removeImpls <$> reify ty
 
+  here <- currentTopLevelModule
   tooltip <- fmap renderToHtml $ P.vcat
-    [ P.hsep [ annotate a <$> P.pretty (qnameName (defName d))
-             , "(" <> kind <> ", defined in " <> topm' <> ")"
-             ]
+    [ annotate a <$> P.pretty (qnameName (defName d))
     , P.nest 2 (P.colon P.<+> prettyATop expr)
     ]
   plain <- Text.pack . render <$> prettyATop expr
@@ -354,27 +341,27 @@ killQual = Con.mapExpr wrap where
   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) =
---   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 [] 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
+removeImpls :: A.Expr -> A.Expr
+removeImpls (A.Pi _ (x :| xs) 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 [] 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

support/shake/app/HTML/Base.hs

@@ -181,7 +181,7 @@ renderSourceFile types opts (HtmlInputSourceFile moduleName fileType sourceCode
     used _ [] = mempty
 
     (order, usedts) = used 0 tokens
-    pageContents = code order onlyCode fileType tokens
+    pageContents = code order onlyCode fileType moduleName tokens
   in
     rnf order `seq`
       ( page opts onlyCode moduleName pageContents
@@ -279,9 +279,10 @@ code
   :: 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
 
@@ -292,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) (aspectsToHtml types (Just 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

support/shake/app/HTML/Render.hs

@@ -66,7 +66,7 @@ renderToHtml = finish . Ppr.fullRenderAnn Ppr.PageMode 100 1.5 cont [] where
   toBlaze (Mark _)   = __IMPOSSIBLE__
   toBlaze (Text t)   = Html.text t
   toBlaze (Node a t) = Html.span do
-    aspectsToHtml mempty Nothing a $
+    aspectsToHtml Nothing mempty Nothing a $
       traverse_ toBlaze t
     unless (null (note a)) do
       Html.span (string (note a)) !! [Attr.class_ "Note"]
@@ -98,8 +98,8 @@ modToFile m ext = Network.URI.Encode.encode $ render (pretty m) <.> ext
 -- 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 :: HashMap Text.Text (Int, Identifier) -> Maybe Int -> Aspects -> Html -> Html
-aspectsToHtml types pos mi =
+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 (<A> tag) with the given attributes around some HTML.
@@ -161,6 +161,7 @@ aspectsToHtml types pos mi =
       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

support/shake/app/Shake/Markdown.hs

@@ -274,6 +274,7 @@ buildMarkdown modname input output = do
   for_ (Map.toList defs) \(key, bs) -> traced ("writing fragment " <> Text.unpack (getMangled key)) 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.
@@ -414,7 +415,10 @@ patchBlock _ (Div ("refs", _, _) body) = do
   pure $ Plain [] -- TODO: pandoc-types 1.23 removed Null
 
 patchBlock _ b@(Div (id, [only], kv) bs) | "definition" == only, not (Text.null id) = do
-  b <$ tell (MarkdownState mempty (Map.singleton (mangleLink id) bs))
+  let
+    isfn (Note _) = True
+    isfn _ = False
+  b <$ tell (MarkdownState mempty (Map.singleton (mangleLink id) (walk (filter (not . isfn)) bs)))
 
 patchBlock _ h = pure h
 

support/web/css/components/popup.scss

@@ -20,6 +20,14 @@
   &:before {
     display: none;
   }
+
+  a.hover-highlight {
+    background-color: unset;
+  }
+}
+
+.popup-hidden {
+  display: none;
 }
 
 @mixin keyframes-for($dir, $dy) {