From fac9e0145fa0e6b352452dc829ebcb0055f9abf1 Mon Sep 17 00:00:00 2001
From: Rob Lorch <lorchrob@gmail.com>
Date: Thu, 9 May 2024 12:48:17 -0500
Subject: [PATCH] Display the correct buttons for imported nodes

---
 src/Kind2.ts    | 8 ++++++--
 src/treeNode.ts | 6 +++++-
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/Kind2.ts b/src/Kind2.ts
index 6217397..ab6329e 100644
--- 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
index 655ee4b..b8e02cc 100644
--- 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";
   }
 }