Oops, forgot to send notification.

FStarLang · Jul 17, 2024 · f0984c9 · f0984c9
1 parent 9b9f670
commit f0984c9
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/client/src/extension.ts b/client/src/extension.ts
@@ -132,10 +132,11 @@ function updateDecorations() {
 	}
 }
 
+let telemetry: TelemetryReporter;
+
 export async function activate(context: ExtensionContext) {
-	const telemetry = new TelemetryReporter(
-		// '160d3440-45e8-47c1-9cf1-ccd46149ff89'
-		'InstrumentationKey=160d3440-45e8-47c1-9cf1-ccd46149ff89;IngestionEndpoint=https://eastus-8.in.applicationinsights.azure.com/;LiveEndpoint=https://eastus.livediagnostics.monitor.azure.com/;ApplicationId=a4e6ffa7-4f8c-47c3-8d7f-0f4dbcf57019'
+	telemetry = new TelemetryReporter(
+		'160d3440-45e8-47c1-9cf1-ccd46149ff89'
 	);
 	telemetry.sendTelemetryEvent('test', {test:'test'});
 
@@ -216,4 +217,5 @@ export async function activate(context: ExtensionContext) {
 
 export async function deactivate() {
 	await client?.stop();
+	await telemetry?.dispose();
 }
diff --git a/server/src/server.ts b/server/src/server.ts
@@ -37,7 +37,7 @@ import { FStar, FStarConfig } from './fstar';
 import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse, FStarPosition, FullBufferQuery } from './fstar_messages';
 import * as path from 'path';
 import { pathToFileURL } from 'url';
-import { statusNotification, FragmentStatus, killAndRestartSolverNotification, restartNotification, verifyToPositionNotification, killAllNotification, TelemetryEventProperties, TelemetryEventMeasurements } from './fstarLspExtensions';
+import { statusNotification, FragmentStatus, killAndRestartSolverNotification, restartNotification, verifyToPositionNotification, killAllNotification, TelemetryEventProperties, TelemetryEventMeasurements, telemetryNotification } from './fstarLspExtensions';
 import { Debouncer, RateLimiter } from './signals';
 
 // LSP Server
@@ -142,7 +142,7 @@ export class Server {
 	}
 
 	sendTelemetryEvent(eventName: string, properties?: TelemetryEventProperties, measurements?: TelemetryEventMeasurements) {
-
+		void this.connection.sendNotification(telemetryNotification, {eventName, properties, measurements});
 	}
 
 	run() {