dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

persist errors in modules

Browse Source
This commit is contained in:
Steve Dunham
2026-02-13 09:58:09 -08:00
parent dcf162684e
commit 4ec199b064
3 changed files with 6 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
newt-vscode-lsp/src/lsp.ts
View File

@@ -59,6 +59,7 @@ function runChange() {
const end = +new Date() const end = +new Date()
connection.sendDiagnostics({uri,diagnostics}) connection.sendDiagnostics({uri,diagnostics})
console.log('CHECK', doc.uri, 'in', end-start); console.log('CHECK', doc.uri, 'in', end-start);
console.log("GOT\n",JSON.stringify(diagnostics, null, ' '))
running = undefined running = undefined
// If we just sent one, it seems that we need to give vscode some time to send the rest // 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. // Otherwise, for Elab.newt, we hit 1.8s for each character typed.

6
src/Lib/ProcessModule.newt
View File

@@ -21,7 +21,7 @@ addPrimitives = do
processDecl primNS (PType emptyFC "Char" Nothing) 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 setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil
top <- getTop 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 let modules = updateMap primNS mod top.modules
modifyTop [ modules := modules modifyTop [ modules := modules
; imported := primNS :: Nil ; imported := primNS :: Nil
@@ -91,7 +91,7 @@ processModule importFC repo stk modns = do
let importNames = map importToName imports let importNames = map importToName imports
imported <- for imports $ \case imported <- for imports $ \case
MkImport fc (nameFC,name') => do MkImport fc (nameFC, name') => do
let imp = split name' "." let imp = split name' "."
when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} → \{show name'}" when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} → \{show name'}"
processModule nameFC repo (name :: stk) imp 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 -- update modules with result, leave the rest of context in case this is top file
top <- getTop 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 let modules = updateMap modns mod top.modules
modifyTop [modules := modules] modifyTop [modules := modules]

3
src/Lib/Types.newt
View File

@@ -403,6 +403,7 @@ record ModContext where
-- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import
ctxOps : Operators ctxOps : Operators
modDeps : List (List String) modDeps : List (List String)
modErrors : List Error
-- Top level context. -- Top level context.
-- Most of the reason this is separate is to have a different type -- 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 -- A placeholder while walking through dependencies of a module
emptyModCtx : String → ModContext 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 : U
HintTable = SortedMap QName (List (QName × Tm)) HintTable = SortedMap QName (List (QName × Tm))