Display the correct buttons for imported nodes

kind2-mc · May 9, 2024 · fac9e01 · fac9e01
1 parent c10c665
commit fac9e01
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/src/Kind2.ts b/src/Kind2.ts
@@ -57,12 +57,16 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
 
         if (component.state.length > 0 && component.state[0] === "running") {
           codeLenses.push(new CodeLens(range, { title: "Cancel", command: "kind2/cancel", arguments: [component] }));
+        } else if (component.imported) {
+          codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }))
         } else {
           codeLenses.push(new CodeLens(range, { title: "Check Properties", command: "kind2/check", arguments: [component] }));
           codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }))
         }
         codeLenses.push(new CodeLens(range, { title: "Simulate", command: "kind2/interpret", arguments: [component, "[]"] }));
-        codeLenses.push(new CodeLens(range, { title: "Raw Output", command: "kind2/raw", arguments: [component] }));
+        if (!component.imported) {
+          codeLenses.push(new CodeLens(range, { title: "Raw Output", command: "kind2/raw", arguments: [component] }));
+        }
         codeLenses.push(new CodeLens(range, { title: "Show in Explorer", command: "kind2/reveal", arguments: [component] }));
       }
     }
@@ -247,7 +251,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
         if (component.contractStartLine === undefined) {
           contractStart = component.startLine - 1;
         }
-        file.components.push(new Component(component.name, component.startLine - 1, contractStart, file));
+        file.components.push(new Component(component.name, component.startLine - 1, contractStart, file, component.imported));
       }
     }
     this._files = this._files.concat(newFiles);

diff --git a/src/treeNode.ts b/src/treeNode.ts
@@ -26,8 +26,11 @@ export type RealizabilitySource = "inputs" | "contract" | "imported node"
 export class Component {
   private _state: State[];
   private _analyses: Analysis[];
+  private _imported: boolean;
   set analyses(analyses: Analysis[]) { this._analyses = analyses; }
   get analyses(): Analysis[] { return this._analyses; }
+  set imported(imported: boolean) { this._imported = imported; }
+  get imported(): boolean { return this._imported; }
   set state(state: State[]) {
     if (this._analyses.length == 0) {
       this._state = state;
@@ -120,9 +123,10 @@ export class Component {
     return this.state.some(str => str.includes("unrealizable"))
   }
   get uri(): string { return this.parent.uri; }
-  constructor(readonly name: string, readonly line: number, readonly contractLine: number, readonly parent: File) {
+  constructor(readonly name: string, readonly line: number, readonly contractLine: number, readonly parent: File, readonly imported_comp: string) {
     this._state = ["pending"];
     this._analyses = [];
+    this._imported = imported_comp === "true";
   }
 }