diff --git a/lake-manifest.json b/lake-manifest.json
index b9ee710..e9b3096 100644
--- 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
index d38b7dc..cda2280 100644
--- 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 {{ {{type}}
}}
| .str s =>
some <$> addHover {{ {{s.quote}}" : String"
}}
+ | .withType t =>
+ some <$> addHover {{ {{t}}
}}
| _ => 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'});