From 6ce666ae493d36c25e05add341895c191b61e8b3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 4 Sep 2024 17:30:58 +0200 Subject: [PATCH] feat: necessary information for tooltips on options in code --- src/highlighting/SubVerso/Highlighting/Code.lean | 4 ++-- src/highlighting/SubVerso/Highlighting/Highlighted.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean index e5cf934..48a0677 100644 --- a/src/highlighting/SubVerso/Highlighting/Code.lean +++ b/src/highlighting/SubVerso/Highlighting/Code.lean @@ -188,8 +188,8 @@ def infoKind [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m] | .ofTermInfo termInfo => termInfoKind ids ci termInfo | .ofFieldInfo fieldInfo => some <$> fieldInfoKind ci fieldInfo | .ofOptionInfo oi => - let docs โ† findDocString? (โ† getEnv) oi.declName - pure <| some <| .option oi.declName docs + let doc := (โ† getOptionDecls).find? oi.optionName |>.map (ยท.descr) + pure <| some <| .option oi.optionName oi.declName doc | .ofCompletionInfo _ => pure none | .ofTacticInfo _ => pure none | _ => diff --git a/src/highlighting/SubVerso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean index 12ef238..58616db 100644 --- a/src/highlighting/SubVerso/Highlighting/Highlighted.lean +++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean @@ -44,7 +44,7 @@ inductive Token.Kind where | const (name : Name) (signature : String) (docs : Option String) | var (name : FVarId) (type : String) | str (string : String) - | option (name : Name) (docs : Option String) + | option (name : Name) (declName : Name) (docs : Option String) | docComment | sort | unknown @@ -56,7 +56,7 @@ instance : Quote Token.Kind where quote | .keyword n occ docs => mkCApp ``keyword #[quote n, quote occ, quote docs] | .const n sig docs => mkCApp ``const #[quote n, quote sig, quote docs] - | .option n docs => mkCApp ``option #[quote n, quote docs] + | .option n d docs => mkCApp ``option #[quote n, quote d, quote docs] | .var (.mk n) type => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n], quote type] | .str s => mkCApp ``str #[quote s] | .docComment => mkCApp ``docComment #[]