diff --git a/package.json b/package.json
index c5864bf..05de6c4 100644
--- a/package.json
+++ b/package.json
@@ -149,6 +149,11 @@
"title": "Display model checking panel",
"category": "TLA+"
},
+ {
+ "command": "tlaplus.model.editor.display",
+ "title": "Display model editor",
+ "category": "TLA+"
+ },
{
"command": "tlaplus.out.visualize",
"title": "Visualize TLC output",
@@ -196,6 +201,10 @@
"command": "tlaplus.model.check.run",
"when": "editorLangId == tlaplus || editorLangId == tlaplus_cfg"
},
+ {
+ "command": "tlaplus.model.editor.display",
+ "when": "editorLangId == tlaplus"
+ },
{
"command": "tlaplus.model.check.runAgain",
"when": "tlaplus.tlc.canRunAgain"
@@ -226,6 +235,11 @@
"command": "tlaplus.model.check.run",
"when": "resourceLangId == tlaplus || resourceLangId == tlaplus_cfg",
"group": "z_commands"
+ },
+ {
+ "command": "tlaplus.model.editor.display",
+ "when": "resourceLangId == tlaplus",
+ "group": "z_commands"
}
],
"editor/context": [
@@ -234,6 +248,11 @@
"when": "editorLangId == tlaplus || editorLangId == tlaplus_cfg",
"group": "z_commands"
},
+ {
+ "command": "tlaplus.model.editor.display",
+ "when": "editorLangId == tlaplus",
+ "group": "z_commands"
+ },
{
"command": "tlaplus.out.visualize",
"when": "resourceExtname == .out",
diff --git a/resources/model-editor-view.css b/resources/model-editor-view.css
new file mode 100644
index 0000000..e3ae241
--- /dev/null
+++ b/resources/model-editor-view.css
@@ -0,0 +1,8 @@
+.constant_definition_input {
+ margin: 0 0 0 9px;
+}
+
+.constant_definition_label {
+ margin: 0 6px;
+}
+
diff --git a/resources/model-editor-view.html b/resources/model-editor-view.html
new file mode 100644
index 0000000..36f7960
--- /dev/null
+++ b/resources/model-editor-view.html
@@ -0,0 +1,89 @@
+
+
+
+
+
+
+
+
+
+
+ Model Editor
+
+
+
+
+
+
+
+
+
+ Init:
+
+ Next:
+
+
+
+
+
+
+
+
+
+
+
diff --git a/resources/model-editor-view.js b/resources/model-editor-view.js
new file mode 100644
index 0000000..2590534
--- /dev/null
+++ b/resources/model-editor-view.js
@@ -0,0 +1,296 @@
+/**
+ * The "client-side" JavaScript code for the model editor web view. Please observe the numerous TODO in
+ * comments below.
+ */
+const vscode = acquireVsCodeApi();
+
+initialize();
+
+function initialize() {
+ window.addEventListener('message', (event) => {
+ if (typeof event.data.modelConstants !== 'undefined') {
+ populateModelConstants(event.data.modelConstants);
+ } else if (typeof event.data.editors !== 'undefined') {
+ populateOpenEditorsList(event.data.editors);
+ }
+ });
+
+ const behaviorSpecSelectElement = document.getElementById("behavior-spec");
+ behaviorSpecSelectElement.addEventListener("change", function() {
+ const selectedBehavior = behaviorSpecSelectElement.options[behaviorSpecSelectElement.selectedIndex].value;
+ const initNextDiv = document.getElementById("init-next-div");
+ const temporalDiv = document.getElementById("temporal-div");
+
+ if (selectedBehavior == "init-next") {
+ initNextDiv.style.display = "block";
+ temporalDiv.style.display = "none";
+ } else if (selectedBehavior == "temporal") {
+ initNextDiv.style.display = "none";
+ temporalDiv.style.display = "block";
+ } else {
+ initNextDiv.style.display = "none";
+ temporalDiv.style.display = "none";
+ }
+
+ validateModelEditorState();
+ });
+
+ wireKeyUpValidation("init-declaration");
+ wireKeyUpValidation("next-declaration");
+ wireKeyUpValidation("temporal-declaration");
+
+ vscode.postMessage({
+ command: 'getOpenEditors'
+ });
+}
+
+// Invoked in response to extension -> view
+function populateModelConstants(modelConstants) {
+ const modelConstantsDiv = document.getElementById('model-constants-div');
+
+ while (modelConstantsDiv.firstChild) {
+ modelConstantsDiv.removeChild(modelConstantsDiv.lastChild);
+ }
+
+ modelConstants.forEach(function (modelConstant) {
+ const divElement = document.createElement("div");
+ divElement.classList.add("constant_definition");
+ divElement.setAttribute("data-constant-name", modelConstant);
+ divElement.appendChild(document.createTextNode(modelConstant + " →"));
+ appendConstantSettingsDiv(divElement, modelConstant + "_");
+ modelConstantsDiv.appendChild(divElement);
+ });
+
+ validateModelEditorState();
+}
+
+// Invoked in response to extension -> view
+function populateOpenEditorsList(editorFilenames) {
+ if (editorFilenames != null) {
+ const editorSelectElement = document.getElementById('editor-chooser');
+
+ editorSelectElement.appendChild(document.createElement("option"));
+ editorFilenames.forEach(function (filename) {
+ const option = document.createElement("option");
+ let index = filename.lastIndexOf('/');
+ if (index == -1) {
+ index = filename.lastIndexOf("\\");
+ }
+ const name = document.createTextNode(filename.substring(index + 1));
+
+ option.setAttribute("value", filename);
+ option.appendChild(name);
+ editorSelectElement.appendChild(option);
+ });
+
+ editorSelectElement.addEventListener("change", function() {
+ const selectedFilename = editorSelectElement.options[editorSelectElement.selectedIndex].value;
+
+ if (selectedFilename) {
+ vscode.postMessage({
+ command: 'getModelConstants',
+ filename: selectedFilename
+ });
+ }
+ });
+ }
+}
+
+// Invoked from view user action
+function startModelCheck() {
+ const behaviorSpecSelectElement = document.getElementById("behavior-spec");
+ const behaviorSpec = new Object();
+ behaviorSpec.kind = behaviorSpecSelectElement.options[behaviorSpecSelectElement.selectedIndex].value;
+ if (behaviorSpec.kind == "init-next") {
+ behaviorSpec.init = document.getElementById("init-declaration").value.trim();
+ behaviorSpec.next = document.getElementById("next-declaration").value.trim();
+ } else if (behaviorSpec.kind == "temporal") {
+ behaviorSpec.temporal = document.getElementById("temporal-declaration").value.trim();
+ }
+
+ const constants = new Array();
+ const constantDivs = document.getElementsByClassName("constant_definition");
+ for (let i = 0; i < constantDivs.length; i++) {
+ const typeRadioElements = constantDivs[i].querySelectorAll("input[name='constant-type']");
+ let selectedRadio = null;
+ for (let j = 0; j < typeRadioElements.length; j++) {
+ if (typeRadioElements[j].checked) {
+ selectedRadio = typeRadioElements[j];
+ break;
+ }
+ }
+
+ const valueTextField = constantDivs[i].querySelector("input[type='text']");
+ const constant = new Object();
+ constant.name = constantDivs[i].getAttribute("data-constant-name");
+ constant.type = selectedRadio.value;
+ constant.value = valueTextField.value;
+ // TODO symmetry set, Type need to be sent across
+
+ constants.push(constant);
+ }
+
+ const editorSelectElement = document.getElementById('editor-chooser');
+ vscode.postMessage({
+ command: 'writeMCFiles',
+ filename: editorSelectElement.options[editorSelectElement.selectedIndex].value,
+ behaviorSpec: behaviorSpec,
+ constants: constants
+ });
+
+ vscode.postMessage({
+ command: 'startModelCheck',
+ filename: editorSelectElement.options[editorSelectElement.selectedIndex].value
+ });
+
+ // In the correctly written version, we should wait for an ACK before hiding this element
+ const modelCheckLinkElement = document.getElementById("action-start-model-check");
+ modelCheckLinkElement.classList.add("hidden");
+ delete modelCheckLinkElement.onclick;
+
+ // TODO In the correctly written version, we should wait for an ACK before showing and arming this element
+ const stopModelCheckLinkElement = document.getElementById("action-stop-model-check");
+ stopModelCheckLinkElement.classList.remove("hidden");
+ stopModelCheckLinkElement.onclick = () => stopModelCheck();
+}
+
+// Invoked from view user action
+function stopModelCheck() {
+ vscode.postMessage({
+ command: 'stopModelCheck'
+ });
+
+ // TODO In the correctly written version, we should wait for an ACK before hiding this element
+ const modelCheckLinkElement = document.getElementById("action-stop-model-check");
+ modelCheckLinkElement.classList.add("hidden");
+ delete modelCheckLinkElement.onclick;
+
+ validateModelEditorState();
+}
+
+function wireKeyUpValidation(id) {
+ const element = document.getElementById(id);
+ element.onkeyup = () => validateModelEditorState();
+}
+
+function validateModelEditorState() {
+ const editorSelectElement = document.getElementById('editor-chooser');
+ const selectedFilename = editorSelectElement.options[editorSelectElement.selectedIndex].value;
+ let canExecute = (selectedFilename && (selectedFilename.length > 0));
+
+ if (canExecute) {
+ const behaviorSpecSelectElement = document.getElementById("behavior-spec");
+ const selectedBehavior = behaviorSpecSelectElement.options[behaviorSpecSelectElement.selectedIndex].value;
+ if (selectedBehavior == "init-next") {
+ const initDeclarationDiv = document.getElementById("init-declaration");
+
+ if (initDeclarationDiv.value.trim().length > 0) {
+ const nextDeclarationDiv = document.getElementById("next-declaration");
+
+ canExecute = (nextDeclarationDiv.value.trim().length > 0);
+ } else {
+ canExecute = false;
+ }
+ } else if (selectedBehavior == "temporal") {
+ const temporalDeclarationDiv = document.getElementById("temporal-declaration");
+
+ canExecute = (temporalDeclarationDiv.value.trim().length > 0);
+ }
+
+ if (canExecute) {
+ const constantTextFields = document.getElementsByClassName("constant_definition_textfield");
+ for (let i = 0; i < constantTextFields.length; i++) {
+ if (constantTextFields[i].value.trim().length == 0) {
+ canExecute = false;
+ break;
+ }
+ }
+ }
+ }
+
+ const modelCheckLinkElement = document.getElementById("action-start-model-check");
+ if (canExecute) {
+ modelCheckLinkElement.classList.remove("hidden");
+ modelCheckLinkElement.onclick = () => startModelCheck();
+ } else {
+ modelCheckLinkElement.classList.add("hidden");
+ delete modelCheckLinkElement.onclick;
+ }
+}
+
+function appendConstantSettingsDiv(divElement, idPrefix) {
+ const textField = document.createElement("input");
+ textField.setAttribute("type", "text");
+ textField.setAttribute("id", idPrefix + "textfield");
+ textField.classList.add('constant_definition_input');
+ textField.classList.add('constant_definition_textfield');
+ textField.onkeyup = () => validateModelEditorState();
+ divElement.appendChild(textField);
+
+ const ordinaryRadio = document.createElement("input");
+ ordinaryRadio.setAttribute("type", "radio");
+ ordinaryRadio.setAttribute("name", "constant-type");
+ ordinaryRadio.setAttribute("value", "ordinary");
+ ordinaryRadio.checked = true;
+ ordinaryRadio.setAttribute("id", idPrefix + "ordinary-radio");
+ ordinaryRadio.classList.add('constant_definition_input');
+ divElement.appendChild(ordinaryRadio);
+ const ordinaryLabel = document.createElement("label");
+ ordinaryLabel.setAttribute("for", idPrefix + "ordinary-radio");
+ ordinaryLabel.appendChild(document.createTextNode("ordinary assignment"));
+ ordinaryLabel.classList.add('constant_definition_label');
+ divElement.appendChild(ordinaryLabel);
+
+ const modelValueRadio = document.createElement("input");
+ modelValueRadio.setAttribute("type", "radio");
+ modelValueRadio.setAttribute("name", "constant-type");
+ modelValueRadio.setAttribute("value", "model-value");
+ modelValueRadio.setAttribute("id", idPrefix + "model-value-radio");
+ modelValueRadio.classList.add('constant_definition_input');
+ divElement.appendChild(modelValueRadio);
+ const modelValueLabel = document.createElement("label");
+ modelValueLabel.setAttribute("for", idPrefix + "model-value-radio");
+ modelValueLabel.appendChild(document.createTextNode("model value"));
+ modelValueLabel.classList.add('constant_definition_label');
+ divElement.appendChild(modelValueLabel);
+
+ const setOfModelValuesRadio = document.createElement("input");
+ setOfModelValuesRadio.setAttribute("type", "radio");
+ setOfModelValuesRadio.setAttribute("name", "constant-type");
+ setOfModelValuesRadio.setAttribute("value", "set-of-model-values");
+ setOfModelValuesRadio.setAttribute("id", idPrefix + "set-of-model-values-radio");
+ setOfModelValuesRadio.classList.add('constant_definition_input');
+ divElement.appendChild(setOfModelValuesRadio);
+ const setOfModelValuesLabel = document.createElement("label");
+ setOfModelValuesLabel.setAttribute("for", idPrefix + "set-of-model-values-radio");
+ setOfModelValuesLabel.appendChild(document.createTextNode("set of model values"));
+ setOfModelValuesLabel.classList.add('constant_definition_label');
+ divElement.appendChild(setOfModelValuesLabel);
+
+ const symmetrySetCheckbox = document.createElement("input");
+ symmetrySetCheckbox.setAttribute("type", "checkbox");
+ symmetrySetCheckbox.setAttribute("value", "symmetry-set");
+ symmetrySetCheckbox.setAttribute("id", idPrefix + "symmetry-set-checkbox");
+ divElement.appendChild(symmetrySetCheckbox);
+ const symmetrySetLabel = document.createElement("label");
+ symmetrySetLabel.setAttribute("for", idPrefix + "symmetry-set-checkbox");
+ symmetrySetLabel.appendChild(document.createTextNode("symmetry set"));
+ divElement.appendChild(symmetrySetLabel);
+
+ const typeCheckbox = document.createElement("input");
+ typeCheckbox.setAttribute("type", "checkbox");
+ typeCheckbox.setAttribute("value", "model-set-type");
+ typeCheckbox.setAttribute("id", idPrefix + "model-set-type-checkbox");
+ divElement.appendChild(typeCheckbox);
+ const typeLabel = document.createElement("label");
+ typeLabel.setAttribute("for", idPrefix + "model-set-type-checkbox");
+ typeLabel.appendChild(document.createTextNode("Type"));
+ divElement.appendChild(typeLabel);
+
+ // TODO type combobox
+ // TODO enable/disable logic on sym set and type
+
+ /*
+constant name -> _value_textfield_ ( ) ordinary assignment ( ) model value ( ) set of model values [ ] symmetry set [ ] Type [A |v]
+ */
+}
diff --git a/src/main.ts b/src/main.ts
index 033dcb2..3c2cb12 100644
--- a/src/main.ts
+++ b/src/main.ts
@@ -5,6 +5,7 @@ import { CMD_CHECK_MODEL_RUN, CMD_CHECK_MODEL_STOP, CMD_CHECK_MODEL_DISPLAY, CMD
showTlcOutput, checkModelCustom, CMD_CHECK_MODEL_RUN_AGAIN, runLastCheckAgain} from './commands/checkModel';
import { CMD_EVALUATE_SELECTION, evaluateSelection, CMD_EVALUATE_EXPRESSION,
evaluateExpression } from './commands/evaluateExpression';
+import { showModelEditor, CMD_MODEL_EDITOR_DISPLAY } from './modelEditorView';
import { parseModule, CMD_PARSE_MODULE } from './commands/parseModule';
import { visualizeTlcOutput, CMD_VISUALIZE_TLC_OUTPUT } from './commands/visualizeOutput';
import { exportModuleToTex, exportModuleToPdf, CMD_EXPORT_TLA_TO_TEX,
@@ -25,6 +26,7 @@ const TLAPLUS_CFG_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', lan
const CHANGELOG_URL = vscode.Uri.parse('https://github.com/alygin/vscode-tlaplus/blob/master/CHANGELOG.md#change-log');
const tlaDocInfos = new TlaDocumentInfos();
+export const symbolsProvider = new TlaDocumentSymbolsProvider(tlaDocInfos);
// Holds all the error messages
let diagnostic: vscode.DiagnosticCollection;
@@ -62,6 +64,9 @@ export function activate(context: vscode.ExtensionContext) {
vscode.commands.registerCommand(
CMD_CHECK_MODEL_DISPLAY,
() => displayModelChecking(context)),
+ vscode.commands.registerCommand(
+ CMD_MODEL_EDITOR_DISPLAY,
+ () => showModelEditor(context)),
vscode.commands.registerCommand(
CMD_VISUALIZE_TLC_OUTPUT,
() => visualizeTlcOutput(context)),
@@ -85,7 +90,7 @@ export function activate(context: vscode.ExtensionContext) {
'\n'),
vscode.languages.registerDocumentSymbolProvider(
TLAPLUS_FILE_SELECTOR,
- new TlaDocumentSymbolsProvider(tlaDocInfos),
+ symbolsProvider,
{ label: 'TLA+' }),
vscode.languages.registerCompletionItemProvider(
TLAPLUS_FILE_SELECTOR,
diff --git a/src/modelEditorView.ts b/src/modelEditorView.ts
new file mode 100644
index 0000000..d5c7fd5
--- /dev/null
+++ b/src/modelEditorView.ts
@@ -0,0 +1,191 @@
+import * as vscode from 'vscode';
+import * as fs from 'fs';
+import * as path from 'path';
+import { CMD_CHECK_MODEL_RUN, CMD_CHECK_MODEL_STOP, checkModel } from './commands/checkModel';
+
+export const CMD_MODEL_EDITOR_DISPLAY = 'tlaplus.model.editor.display';
+
+// Cached HTML template for the WebView
+let viewHtml: string | undefined;
+let viewPanel: vscode.WebviewPanel | undefined;
+
+/**
+ * This is the extension side of the Model Editor web view. It currently supports only the most
+ * base of situations: behavior spec of type temporal and ordinary assignments for constant
+ * values. This was written as a quick proof of concept.
+ *
+ * Observe comments notes below.
+ */
+
+
+export function showModelEditor(extContext: vscode.ExtensionContext) {
+ if (!viewPanel) {
+ createNewPanel();
+ ensurePanelBody(extContext);
+ } else {
+ viewPanel.reveal();
+ }
+}
+
+function createNewPanel() {
+ const title = 'TLA+ Model Editor';
+ viewPanel = vscode.window.createWebviewPanel(
+ 'modelEditor',
+ title,
+ vscode.ViewColumn.Beside,
+ {
+ enableScripts: true,
+ localResourceRoots: [vscode.Uri.file(path.resolve(__dirname, '../../resources'))]
+ }
+ );
+ viewPanel.iconPath = {
+ dark: vscode.Uri.file(path.resolve(__dirname, '../../resources/images/preview-dark.svg')),
+ light: vscode.Uri.file(path.resolve(__dirname, '../../resources/images/preview-light.svg')),
+ };
+ viewPanel.onDidDispose(() => {
+ viewPanel = undefined;
+ });
+ viewPanel.webview.onDidReceiveMessage(message => {
+ if (message.command === 'getOpenEditors') {
+ if (viewPanel && viewPanel.visible) {
+ // TODO for no clear reason "visible text editors" do not appear to include
+ // open text editors in tabs that do not have the focus in their
+ // pane.
+ const textEditors = vscode.window.visibleTextEditors;
+ const openEditorFilenames = new Array();
+ textEditors.forEach(function(editor) {
+ const filename = editor.document.fileName;
+
+ if (filename.toLowerCase().endsWith("tla")) {
+ openEditorFilenames.push(filename);
+ }
+ });
+ viewPanel.webview.postMessage({
+ editors: openEditorFilenames
+ });
+ }
+ } else if (message.command === 'getModelConstants') {
+ if (viewPanel && viewPanel.visible) {
+ const editorFilename = message.filename;
+ const textEditors = vscode.window.visibleTextEditors;
+ let textEditor = null;
+ for (let i = 0; i < textEditors.length; i++) {
+ if (textEditors[i].document.fileName == editorFilename) {
+ textEditor = textEditors[i];
+ break;
+ }
+ }
+
+ const constantsList = new Array();
+ if (textEditor) {
+ for (let i = 0; i < textEditor.document.lineCount; ++i) {
+ const line = textEditor.document.lineAt(i);
+ const matches = /^[\s]*CONSTANT[S]?\s([a-zA-Z0-9\s\-,_]*)[\\\*]?.*$/g.exec(line.text);
+ if (matches) {
+ const names = matches[1].trim().split(',');
+ Array.prototype.push.apply(constantsList, names);
+ }
+ }
+ }
+ viewPanel.webview.postMessage({
+ modelConstants: constantsList
+ });
+ }
+ } else if (message.command === 'stopModelCheck') {
+ vscode.commands.executeCommand(CMD_CHECK_MODEL_STOP);
+ } else if (message.command === 'startModelCheck') {
+ const mcFilenames = mcFilenamesFromSpecFilename(message.filename);
+ const mcTLAUri = vscode.Uri.file(mcFilenames[0]);
+ vscode.commands.executeCommand(CMD_CHECK_MODEL_RUN, mcTLAUri);
+ } else if (message.command === 'writeMCFiles') {
+ const constants = message.constants;
+ const spec = message.behaviorSpec;
+ const filename = message.filename;
+ const lastSeparatorIndex = filename.lastIndexOf(path.sep);
+ const moduleName = filename.substring((lastSeparatorIndex + 1), (filename.length - 4));
+ const mcFilenames = mcFilenamesFromSpecFilename(filename);
+
+ if (writeMCFiles(mcFilenames[0], mcFilenames[1], moduleName, constants, spec)) {
+ // TODO send ACK
+ } else {
+ // TOOO send NACK
+ }
+ } else if (message.command === 'showErrorMessage') {
+ vscode.window.showErrorMessage(message.text);
+ } else if (message.command === 'showInfoMessage') {
+ vscode.window.showInformationMessage(message.text);
+ }
+ });
+}
+
+function ensurePanelBody(extContext: vscode.ExtensionContext) {
+ if (!viewPanel) {
+ return;
+ }
+ if (!viewHtml) {
+ const resourcesDiskPath = vscode.Uri.file(
+ path.join(extContext.extensionPath, 'resources')
+ );
+ const resourcesPath = viewPanel.webview.asWebviewUri(resourcesDiskPath);
+ viewHtml = fs.readFileSync(path.join(extContext.extensionPath, 'resources', 'model-editor-view.html'), 'utf8');
+ viewHtml = viewHtml
+ .replace(/\${cspSource}/g, viewPanel.webview.cspSource)
+ .replace(/\${resourcesPath}/g, String(resourcesPath));
+ }
+ viewPanel.webview.html = viewHtml;
+}
+
+function mcFilenamesFromSpecFilename(filename: string) {
+ const lastSeparatorIndex = filename.lastIndexOf(path.sep);
+ const parentDirectory = filename.substring(0, lastSeparatorIndex);
+ const filenames = new Array();
+
+ filenames.push(parentDirectory + path.sep + "MC.tla");
+ filenames.push(parentDirectory + path.sep + "MC.cfg");
+
+ return filenames;
+}
+
+// TODO see file head comments concerning the only supported case at the moment
+function writeMCFiles(mcTLAFile: string, mcCFGFile: string, moduleName: string, constants: Array, spec: any) {
+ let tlaConstantRun = "";
+ let cfgConstantRun = "";
+ let constantUniquer = 1;
+ constants.forEach(function (constant) {
+ const definition = "const_" + constantUniquer;
+ tlaConstantRun += definition + " == " + constant.value + "\n";
+ cfgConstantRun += "CONSTANT " + constant.name + " <- " + definition + "\n";
+ constantUniquer++;
+ });
+
+ if (spec.kind == "temporal") {
+ cfgConstantRun += "SPECIFICATION " + spec.temporal + "\n";
+ } else if (spec.kind == "init-next") {
+ cfgConstantRun += "INIT " + spec.init + "\n";
+ cfgConstantRun += "NEXT " + spec.next + "\n";
+ }
+
+
+ const specification = "---- MODULE MC ----\nEXTENDS " + moduleName + ", TLC\n"
+ + tlaConstantRun
+ + "\n====================\n";
+ fs.writeFile(mcTLAFile, specification, function (err) {
+ if (err) {
+ vscode.window.showErrorMessage("Problem encountered writing MC.tla: " + err);
+
+ return false;
+ }
+ });
+
+ fs.writeFile(mcCFGFile, cfgConstantRun, function (err) {
+ if (err) {
+ vscode.window.showErrorMessage("Problem encountered writing MC.cfg: " + err);
+
+ // TODO delete MC.tla
+
+ return false;
+ }
+ });
+
+ return true;
+}
diff --git a/tools/tla2tools.jar b/tools/tla2tools.jar
index 5655655..8aeb1a6 100644
Binary files a/tools/tla2tools.jar and b/tools/tla2tools.jar differ