Revert "Merge diagnostics from lax process."

This reverts commit bb544c3.

.eslintrc.js

@@ -21,6 +21,5 @@ module.exports = {
 		'@typescript-eslint/explicit-module-boundary-types': 0,
 		'@typescript-eslint/no-non-null-assertion': 0,
 		'@typescript-eslint/no-floating-promises': 1,
-		'no-inner-declarations': 0,
 	}
 };

server/src/server.ts

@@ -403,17 +403,9 @@ export class DocumentState {
 			[...this.fstar.results.diagnostics, ...this.fstar.results.outOfBandErrors];
 
 		if (this.fstar_lax) {
-			// Merge diagnostics from the lax process.
-			// Note: pulse produces *different* diagnostics in the lax process,
-			// in particular `show_proof_state` might only be available there and not in the full process.
-			// Therefore we need to merge diagnostics even for fragments
-			// which have been processed by both the lax and full processes.
-			function rangeStr(r: Range): string { return `${r.start.line}:${r.start.character}-${r.end.line}:${r.end.character}`; }
-			const existingRanges = new Set<string>();
-			for (const diag of this.fstar.results.diagnostics) {
-				existingRanges.add(rangeStr(diag.range));
-			}
-			diags.push(...this.fstar_lax.results.diagnostics.filter(d => !existingRanges.has(rangeStr(d.range))));
+			// Add diagnostics from the lax position that are after the part processed by the full process.
+			const lastPos = mkPosition(this.fstar.results.fragments.findLast(f => !f.invalidatedThroughEdits && f.ok !== undefined)?.range?.end || [1, 1]);
+			diags.push(...this.fstar_lax.results.diagnostics.filter(d => posLe(lastPos, d.range.start)));
 		}
 
 		void this.server.connection.sendDiagnostics({