From e1d83556ae1bf6488a5d30a8260b032ab26b9ded Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 12 Feb 2026 21:59:56 -0800 Subject: [PATCH] LSP jump to definition --- TODO.md | 9 +++++++-- newt-vscode-lsp/src/lsp.ts | 18 ++++++++++++++---- newt-vscode-lsp/src/newt.d.ts | 8 ++++++-- src/Commands.newt | 4 ++-- src/LSP.newt | 21 +++++++++++++-------- src/Lib/Elab.newt | 6 ++---- 6 files changed, 44 insertions(+), 22 deletions(-) diff --git a/TODO.md b/TODO.md index 1a991a7..18586fb 100644 --- a/TODO.md +++ b/TODO.md @@ -1,17 +1,20 @@ ## TODO -- [ ] Inject markdown highlighter into /- -/ comments in vscode +- [ ] Importing Prelude twice should be an error (currently it causes double hints and breaks auto) - [ ] For errors in other files, point to the import - - put a try in there and remove exitFailure - [x] Unsolved metas should be errors (user metas are fine) - [x] Better syntax for forward declared data (so we can distinguish from functions) - [ ] maybe allow "Main" module name for any file +- [ ] Restore "add missing cases" for LSP mode +- [ ] Case split for LSP mode +- [ ] Leverage LSP code for web playground - [ ] Improve handling of names: - We need FC on names in a lot of places - [x] FC for duplicate `data`, `record`, `class` name is wrong (points to `data`) - [x] FC on bad import should point to the name - [x] Current module overrides imports + - [ ] Duplicate data constructors point to `data` - [ ] Allow Qualified names in surface syntax - Don't disambiguate on type for now - [x] change "in prefix position" and "trailing operator" errors to do sections @@ -33,6 +36,8 @@ - We might get into a situation where solving immediately would have gotten us more progress? - [ ] "Failed to unify %var0 and %var1" - get names in there - Need fancier `Env` or the index on the type of `Tm` + - Or the name on the VVar? + - Also we should render %pi, etc more readably (bonus points for _×_) - Editor support: - [ ] add missing cases should skip indented lines - [ ] add missing cases should handle `_::_` diff --git a/newt-vscode-lsp/src/lsp.ts b/newt-vscode-lsp/src/lsp.ts index 39726d9..aeb7cad 100644 --- a/newt-vscode-lsp/src/lsp.ts +++ b/newt-vscode-lsp/src/lsp.ts @@ -15,6 +15,7 @@ import { InitializeParams, InitializeResult, TextDocumentSyncKind, + Location, } from "vscode-languageserver/node"; import { TextDocument } from "vscode-languageserver-textdocument"; @@ -69,16 +70,25 @@ connection.onHover((params): Hover | null => { const uri = params.textDocument.uri; const pos = params.position; console.log('HOVER', uri, pos) - let value = LSP_hoverInfo(uri, pos.line, pos.character) - if (!value) return null - console.log('HOVER is ', value) - return { contents: { kind: "plaintext", value } }; + let res = LSP_hoverInfo(uri, pos.line, pos.character) + if (!res) return null + console.log('HOVER is ', res) + return { contents: { kind: "plaintext", value: res.info } }; }); +connection.onDefinition((params): Location | null => { + const uri = params.textDocument.uri; + const pos = params.position; + let value = LSP_hoverInfo(uri, pos.line, pos.character) + if (!value) return null; + return value.location +}) + connection.onInitialize((_params: InitializeParams): InitializeResult => ({ capabilities: { textDocumentSync: TextDocumentSyncKind.Incremental, hoverProvider: true, + definitionProvider: true, }, })); diff --git a/newt-vscode-lsp/src/newt.d.ts b/newt-vscode-lsp/src/newt.d.ts index c990524..7298051 100644 --- a/newt-vscode-lsp/src/newt.d.ts +++ b/newt-vscode-lsp/src/newt.d.ts @@ -1,5 +1,9 @@ -import { Diagnostic } from "vscode-languageserver"; +import { Diagnostic, Location } from "vscode-languageserver"; export function LSP_updateFile(name: string, content: string): (eta: any) => any; export function LSP_checkFile(name: string): Diagnostic[]; -export function LSP_hoverInfo(name: string, row: number, col: number): string|null; +interface HoverResult { + info: string + location: Location +} +export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult|null; diff --git a/src/Commands.newt b/src/Commands.newt index a686483..796afe8 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -24,7 +24,7 @@ decomposeName fn = -- The cheap version of type at point, find the token, lookup in global context -- Later we will either get good FC for entries or scan them all and build a cache. -getHoverInfo : FileSource → List String → Int → Int → M (Maybe String) +getHoverInfo : FileSource → List String → Int → Int → M (Maybe (String × FC)) getHoverInfo repo modns row col = do mod <- processModule emptyFC repo Nil modns -- not necessarily loaded into top... (Maybe push this down into that branch of processModule) @@ -39,7 +39,7 @@ getHoverInfo repo modns row col = do -- Lookup the name let (Just e) = lookupRaw name top | _ => pure Nothing - pure $ Just "\{show e.name} : \{rpprint Nil e.type}" + pure $ Just ("\{show e.name} : \{rpprint Nil e.type}", e.fc) where getTok : List BTok → Maybe String diff --git a/src/LSP.newt b/src/LSP.newt index 5b17ef6..d88e465 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -79,6 +79,14 @@ updateFile fn src = unsafePerformIO $ do -- modifyIORef state [ topContext := ctx ] modifyIORef state $ \a => [ topContext := ctx ] a + +fcToRange : FC → Json +fcToRange (MkFC uri (MkBounds sr sc er ec)) = + JsonObj $ ("start", mkPosition sr sc) :: ("end", mkPosition er (ec + 1)) :: Nil + where + mkPosition : Int → Int → Json + mkPosition l c = JsonObj $ ("line", JsonInt l) :: ("character", JsonInt c) :: Nil + hoverInfo : String → Int → Int → JSObject hoverInfo uri line col = unsafePerformIO $ do let (base,modns) = decomposeName uri @@ -87,27 +95,24 @@ hoverInfo uri line col = unsafePerformIO $ do if (st.baseDir /= base) then resetState base else pure MkUnit - Right (_, Just msg) <- (getHoverInfo lspFileSource modns line col).runM st.topContext + Right (_, Just (msg, fc)) <- (getHoverInfo lspFileSource modns line col).runM st.topContext | Right _ => do putStrLn $ "Nothing to see here" pure $ jsonToJObject JsonNull | Left err => do putStrLn $ showError "" err pure $ jsonToJObject JsonNull - pure $ jsonToJObject $ JsonStr msg + let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil + pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil errorToDiag : Error -> Json -errorToDiag (E (MkFC fn (MkBounds sr sc er ec)) msg) = +errorToDiag (E fc msg) = JsonObj $ ("severity", JsonInt 1) - -- PARSER `$` is winning over `,`, which is not what I'm expecting Maybe `,` should be special... - :: ("range", (JsonObj $ ("start", range sr sc) :: ("end", range er (ec + 1)) :: Nil)) + :: ("range", fcToRange fc) :: ("message", JsonStr msg) :: ("source", JsonStr "newt") -- what is this key for? :: Nil - where - range : Int → Int → Json - range l c = JsonObj $ ("line", JsonInt l) :: ("character", JsonInt c) :: Nil -- These shouldn't escape errorToDiag (Postpone fc qn msg) = errorToDiag $ E fc "Postpone \{show qn} \{msg}" diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 4c61b4f..fe4ca6e 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -440,10 +440,8 @@ solve env m sp t = do -- let someone else solve this and then check again. debug $ \ _ => "CONSTRAINT2 \{show ix} \{show sp} =?= \{show t}" addConstraint env m sp t - E fc msg => throwError (E fc "\{msg} for \{show ix} \{show sp} =?= \{show t}") - -- debug $ \ _ => "CONSTRAINT3 \{show ix} \{show sp} =?= \{show t}" - -- debug $ \ _ => "because \{showError "" err}" - -- addConstraint env m sp t + -- replace with wrapper + err => throwError (E (getFC err) "\{errorMsg err} for \{show ix} \{show sp} =?= \{show t}") ) unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult