Initial implementation of module imports for simple EXTENDS

Currently, the idea is that imported modules will be searched for based on the URL of the given specification path argument. So, if a spec is loaded from `<url>/spec.tla`, then an imported module M will be searched for and fetched from `<url>/M.tla`. This is an attempt to emulate the module import behavior of TLC i.e., modules that exist in the same directory as a root module should be automatically discovered. Eventually this could be generalized to fetch modules from additional, user-specified locations.

js/app.js

@@ -199,11 +199,11 @@ function componentChooseConstants() {
     if (_.isEmpty(model.specConsts)) {
         return m("span", {}, "");
     }
-    console.log("Instantiating spec constants.");
+    // console.log("Instantiating spec constants.");
 
     let chooseConstsElems = [];
     for (const constDecl in model.specConsts) {
-        console.log(constDecl);
+        // console.log(constDecl);
         let newDiv = m("div", {}, [
             m("span", {}, m.trust("CONSTANT " + constDecl + " ← ")),
             m("input", {
@@ -664,6 +664,8 @@ function componentTraceViewerState(state, ind, isLastState) {
     // Trace expression values, if any are present.
     let traceExprRows = model.traceExprs.map((expr, ind) => {
         let ctx = new Context(null, state, model.specDefs, {}, model.specConstVals);
+        // TODO: Will eventually need to propagate through cached module table in these expression evaluations,
+        // to support evaluation of expressions that may be defined in imported modules.
         let exprVal = evalExprStrInContext(ctx, expr);
         console.log("exprVal:", exprVal);
         let cols = [
@@ -755,42 +757,8 @@ function componentTraceViewer() {
     return m("div", { id: "trace" }, traceElems);
 }
 
-async function handleCodeChange(editor, changes) {
-    console.log("handle code change");
-
-    // Enable resizable panes (experimental).
-    // $( "#initial-states" ).resizable({handles:"s"});
-
-    $("#code-input-pane").resizable({
-        handles: "e",
-        // alsoResize: "#explorer-pane",
-        // handles: {"e": ".splitter"},
-        // handleSelector: ".splitter",
-        resizeHeight: false,
-    });
-
-    // $( "#explorer-pane" ).resizable({
-    // handles:"w"
-    // });
-
-    // Remove any existing line error highlights.
-    var nlines = codeEditor.lineCount();
-    for (var i = 0; i < nlines; i++) {
-        codeEditor.removeLineClass(i, "background");
-    }
-
-    const newText = codeEditor.getValue() + '\n';
-    const edits = tree && changes && changes.map(treeEditForEditorChange);
-
-    const start = performance.now();
-    if (edits) {
-        for (const edit of edits) {
-            tree.edit(edit);
-        }
-    }
-
-    let parsedSpecTree;
-    parsedSpecTree = parseSpec(newText, model.specPath);
+// Called when an updated spec is finished being re-parsed.
+function onSpecParse(newText, parsedSpecTree){
 
     model.specText = newText;
     model.specTreeObjs = parsedSpecTree;
@@ -825,11 +793,56 @@ async function handleCodeChange(editor, changes) {
         return;
     }
 
-    const duration = (performance.now() - start).toFixed(1);
+    // const duration = (performance.now() - startTime).toFixed(1);
 
     reloadSpec();
 }
 
+async function handleCodeChange(editor, changes) {
+    console.log("handle code change");
+
+    // Enable resizable panes (experimental).
+    // $( "#initial-states" ).resizable({handles:"s"});
+
+    $("#code-input-pane").resizable({
+        handles: "e",
+        // alsoResize: "#explorer-pane",
+        // handles: {"e": ".splitter"},
+        // handleSelector: ".splitter",
+        resizeHeight: false,
+    });
+
+    // $( "#explorer-pane" ).resizable({
+    // handles:"w"
+    // });
+
+    // Remove any existing line error highlights.
+    var nlines = codeEditor.lineCount();
+    for (var i = 0; i < nlines; i++) {
+        codeEditor.removeLineClass(i, "background");
+    }
+
+    const newText = codeEditor.getValue() + '\n';
+    const edits = tree && changes && changes.map(treeEditForEditorChange);
+
+    const start = performance.now();
+    if (edits) {
+        for (const edit of edits) {
+            tree.edit(edit);
+        }
+    }
+
+    let parsedSpecTree;
+    // parsedSpecTree = parseSpec(newText, model.specPath);
+
+    let spec = new TLASpec(newText, model.specPath);
+    return spec.parse().then(function(){
+        console.log("SPEC WAS PARSED.", spec);
+        onSpecParse(newText, spec.spec_obj);
+        m.redraw(); //explicitly re-draw on promise resolution.
+    });
+}
+
 function resetTrace() {
     reloadSpec();
     updateTraceRouteParams();
@@ -1116,25 +1129,26 @@ async function loadApp() {
             $codeEditor.CodeMirror.on("changes", () => {
                 // CodeMirror listeners are not known to Mithril, so trigger an explicit redraw after
                 // processing the code change.
-                handleCodeChange();
-                m.redraw();
-
-                // Load constants if given.
-                let constantParams = m.route.param("constants");
-                if (constantParams) {
-                    console.log("CONSTNS:", constantParams);
-                    model.specConstInputVals = constantParams;
-                    setConstantValues();
-                }
+                handleCodeChange().then(function(){
+                    // Load constants if given.
+                    let constantParams = m.route.param("constants");
+                    if (constantParams) {
+                        console.log("CONSTNS:", constantParams);
+                        model.specConstInputVals = constantParams;
+                        setConstantValues();
+                    }
 
-                // Load trace if given.
-                let traceParamStr = m.route.param("trace")
-                if (traceParamStr) {
-                    traceParams = traceParamStr.split(",");
-                    for (const stateHash of traceParams) {
-                        chooseNextState(stateHash);
+                    // Load trace if given.
+                    let traceParamStr = m.route.param("trace")
+                    if (traceParamStr) {
+                        traceParams = traceParamStr.split(",");
+                        for (const stateHash of traceParams) {
+                            chooseNextState(stateHash);
+                        }
                     }
-                }
+                    m.redraw();
+
+                })
             });
             $codeEditor.CodeMirror.setValue(spec);
         }