phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update FileWorker.lean

Browse Source
This commit is contained in:
Pietro Monticone
2023-10-26 17:19:53 +02:00
parent 2951747d1a
commit 3416b32ddc
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/FileWorker.lean
+2 -2
View File
@@ -292,7 +292,7 @@ where
-- TODO(MH): check for interrupt with increased precision -- TODO(MH): check for interrupt with increased precision
cancelTk.check cancelTk.check
/- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
while prefering newer versions over old ones. The former is necessary because we do while preferring newer versions over old ones. The former is necessary because we do
not explicitly clear older diagnostics, while the latter is necessary because we do not explicitly clear older diagnostics, while the latter is necessary because we do
not guarantee that diagnostics are emitted in order. Specifically, it may happen that not guarantee that diagnostics are emitted in order. Specifically, it may happen that
we interrupted this elaboration task right at this point and a newer elaboration task we interrupted this elaboration task right at this point and a newer elaboration task
@@ -300,7 +300,7 @@ where
the interrupt. Explicitly clearing diagnostics is difficult for a similar reason, the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
because we cannot guarantee that no further diagnostics are emitted after clearing because we cannot guarantee that no further diagnostics are emitted after clearing
them. -/ them. -/
-- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
-- because empty diagnostics clear existing error/information squiggles. Therefore we always -- because empty diagnostics clear existing error/information squiggles. Therefore we always
-- want to publish in case there was previously a message at this position. -- want to publish in case there was previously a message at this position.
publishDiagnostics m snap.diagnostics.toArray ctx.hOut publishDiagnostics m snap.diagnostics.toArray ctx.hOut