From 4ec199b064e8ec9cd4701c7bee400449a218e5f5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 13 Feb 2026 09:58:09 -0800 Subject: [PATCH] persist errors in modules --- newt-vscode-lsp/src/lsp.ts | 1 + src/Lib/ProcessModule.newt | 6 +++--- src/Lib/Types.newt | 3 ++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/newt-vscode-lsp/src/lsp.ts b/newt-vscode-lsp/src/lsp.ts index a4c78c2..bad95b6 100644 --- a/newt-vscode-lsp/src/lsp.ts +++ b/newt-vscode-lsp/src/lsp.ts @@ -59,6 +59,7 @@ function runChange() { const end = +new Date() connection.sendDiagnostics({uri,diagnostics}) console.log('CHECK', doc.uri, 'in', end-start); + console.log("GOT\n",JSON.stringify(diagnostics, null, ' ')) running = undefined // If we just sent one, it seems that we need to give vscode some time to send the rest // Otherwise, for Elab.newt, we hit 1.8s for each character typed. diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index c06712e..4d59240 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -21,7 +21,7 @@ addPrimitives = do processDecl primNS (PType emptyFC "Char" Nothing) setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil top <- getTop - let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil + let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil top.errors let modules = updateMap primNS mod top.modules modifyTop [ modules := modules ; imported := primNS :: Nil @@ -91,7 +91,7 @@ processModule importFC repo stk modns = do let importNames = map importToName imports imported <- for imports $ \case - MkImport fc (nameFC,name') => do + MkImport fc (nameFC, name') => do let imp = split name' "." when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} → \{show name'}" processModule nameFC repo (name :: stk) imp @@ -125,7 +125,7 @@ processModule importFC repo stk modns = do -- update modules with result, leave the rest of context in case this is top file top <- getTop - let mod = MkModCtx src top.defs top.metaCtx top.ops importNames + let mod = MkModCtx src top.defs top.metaCtx top.ops importNames top.errors let modules = updateMap modns mod top.modules modifyTop [modules := modules] diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 69fa001..c2d96f8 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -403,6 +403,7 @@ record ModContext where -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import ctxOps : Operators modDeps : List (List String) + modErrors : List Error -- Top level context. -- Most of the reason this is separate is to have a different type @@ -413,7 +414,7 @@ record ModContext where -- A placeholder while walking through dependencies of a module emptyModCtx : String → ModContext -emptyModCtx csum = MkModCtx csum emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil +emptyModCtx csum = MkModCtx csum emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil Nil HintTable : U HintTable = SortedMap QName (List (QName × Tm))