fix: don't show _root_ in code hovers when not needed (#280)

leanprover · Jan 31, 2025 · da3e91c · da3e91c
1 parent d9c0352
commit da3e91c
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b4dd804a58961657d6c2f24d5eb350abb4992204",
+   "rev": "2b9273de4a820dd9f5024875d27372b440c9d981",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean
@@ -258,6 +258,8 @@ defmethod Token.Kind.hover? (tok : Token.Kind) : HighlightHtmlM (Option Nat) :=
     some <$> addHover {{ <code>{{type}}</code> }}
   | .str s =>
     some <$> addHover {{ <code><span class="literal string">{{s.quote}}</span>" : String"</code>}}
+  | .withType t =>
+    some <$> addHover {{ <code>{{t}}</code> }}
   | _ => pure none
 where
   separatedDocs txt :=
@@ -278,6 +280,7 @@ defmethod Token.Kind.«class» : Token.Kind → String
   | .keyword .. => "keyword"
   | .anonCtor .. => "unknown"
   | .unknown => "unknown"
+  | .withType .. => "typed"
 
 defmethod Token.Kind.data : Token.Kind → String
   | .const n _ _ _ | .anonCtor n _ _ => "const-" ++ toString n
@@ -534,7 +537,7 @@ def highlightingStyle : String := "
 }
 
 @media (hover: hover) {
-  .hl.lean .token.binding-hl, .hl.lean .literal.string:hover {
+  .hl.lean .token.binding-hl, .hl.lean .literal.string:hover, .hl.lean .token.typed:hover {
     background-color: #eee;
     border-radius: 2px;
     transition: none;
@@ -1078,7 +1081,7 @@ window.onload = () => {
       const addTippy = (selector, props) => {
         tippy(selector, Object.assign({}, defaultTippyProps, props));
       };
-      addTippy('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token', {theme: 'lean'});
+      addTippy('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token', {theme: 'lean'});
       addTippy('.hl.lean .has-info.warning', {theme: 'warning message'});
       addTippy('.hl.lean .has-info.info', {theme: 'info message'});
       addTippy('.hl.lean .has-info.error', {theme: 'error message'});