merge dev

src/Script/Script.ts

@@ -58,9 +58,10 @@ export class Script {
   download(): void {
     const filename = this.filename + ".js";
     const file = new Blob([this.code], { type: "text/plain" });
-    if (window.navigator.msSaveOrOpenBlob) {
+    const navigator = window.navigator as any;
+    if (navigator.msSaveOrOpenBlob) {
       // IE10+
-      window.navigator.msSaveOrOpenBlob(file, filename);
+      navigator.msSaveOrOpenBlob(file, filename);
     } else {
       // Others
       const a = document.createElement("a"),
@@ -112,6 +113,10 @@ export class Script {
     this.markUpdated();
   }
 
+  imports(): string[] {
+    return [];
+  }
+
   // Serialize the current object to a JSON save state
   toJSON(): any {
     return Generic_toJSON("Script", this);