[bugfix] Typescript errors

jscoq · Jul 26, 2023 · 64fddcb · 64fddcb
1 parent 8c6f579
commit 64fddcb
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 9 deletions.
diff --git a/frontend/classic/js/contextual-info.ts b/frontend/classic/js/contextual-info.ts
@@ -156,7 +156,9 @@ export class CoqContextualInfo {
     }
 
     async _query(command, title) {
+        /** @todo how do you execute queries in coq-lsp? */
         try {
+            // @ts-ignore
             var result = await this.coq.queryPromise(0, ['Vernac', command]);
             return {pp: this.formatMessages(result), status: 'ok'}
         }

diff --git a/frontend/classic/js/settings.ts b/frontend/classic/js/settings.ts
@@ -44,19 +44,20 @@ export class SettingsPanel {
     active : ReactiveVar<boolean>;
     onAction : (ev : { action: string }) => void;
 
-    constructor(model) {
+    constructor(model?: CoqSettings) {
         this.el = $(this.html());
-        this.model = model || new CoqSettings();
+        this.model = model ?? new CoqSettings();
         this.active = new ReactiveVar(false);
         /** @type {(ev: {action: string}) => void} */
         this.onAction = () => {};
 
         this.el.find('#settings--theme').on('change',
-            (ev) => {
+            (ev: JQuery.ChangeEvent<HTMLInputElement>) => {
                 this.model.theme.value = ev.target.checked ? 'light' : 'dark';
         });
-        this.el.find('#settings--company').on('change', ev => {
-            this.model.company.value = ev.target.checked;
+        this.el.find('#settings--company').on('change', 
+            (ev: JQuery.ChangeEvent<HTMLInputElement>) => {
+                this.model.company.value = ev.target.checked;
         });
         this.el.find('.link-to-quick-help').on('click', (/** @type {MouseEvent} */ ev) => {
             this.onAction({action: 'quick-help'});
@@ -65,23 +66,23 @@ export class SettingsPanel {
         });
         // clickaway trick
         this.el.on('blur', ev => {
-            if (this.el.has(ev.originalEvent.relatedTarget).length)
+            if (this.el.has(ev.originalEvent.relatedTarget as Element).length)
                 setTimeout(() => this.el[0].focus(), 1);
             else
                 this.hide();
         });
     }
 
     configure(options) {
-        var v;
+        var v: any;
         if (v = options.theme) {
             this.el.attr('data-theme', v);
             this.model.theme.value = v;
-            this.el.find('#settings--theme').attr('checked', v == 'light');
+            this.el.find('#settings--theme').prop('checked', v == 'light');
         }
         if ((v = options.company) !== undefined) {
             this.model.company.value = v;
-            this.el.find('#settings--company').attr('checked', v);
+            this.el.find('#settings--company').prop('checked', v);
         }
     }
 

diff --git a/frontend/node/src/headless.ts b/frontend/node/src/headless.ts
@@ -1,3 +1,8 @@
+// @ts-nocheck
+/**
+ * The headless manager is broken with coq-lsp backend.
+ * All the calls need to be readjusted to the new document model.
+ */
 import fs from 'fs';
 import os from 'os';
 import path from 'path';