Comments (6)
@afonsonf Do you have plans to re-add the functionality that shows deleted set elements in the error trace view?
vscode-tlaplus/resources/check-result-view.js
Lines 334 to 336 in 0e16f40
Hi, true I missed that part in the migration of the ui, I will add it back
from vscode-tlaplus.
Perhaps it's TLC that should provide annotations in its textual error trace to free IDEs from parsing and evaluating values.
from vscode-tlaplus.
The Toolbox's set difference algorithm:
from vscode-tlaplus.
@afonsonf Do you have plans to re-add the functionality that shows deleted set elements in the error trace view?
vscode-tlaplus/resources/check-result-view.js
Lines 334 to 336 in 0e16f40
from vscode-tlaplus.
Incomplete attempt to bring the rest of the Toolbox diffing over:
diff --git a/src/model/check.ts b/src/model/check.ts
index 79c015a..bf60526 100644
--- a/src/model/check.ts
+++ b/src/model/check.ts
@@ -178,6 +178,14 @@ export class Value {
format(indent: string): string {
return `${this.str}`;
}
+
+ diff(other: Value): boolean {
+ if (this.str !== other.str) {
+ other.setModified();
+ return true;
+ }
+ return false;
+ }
}
/**
@@ -257,6 +265,63 @@ export abstract class CollectionValue extends Value {
formatKey(indent: string, value: Value): string {
return `${indent}${value.key}: `;
}
+
+ // diff(other: Value): boolean {
+ // return false;
+ // }
+ setElementArrayDiffInfo(
+ t: CollectionValue,
+ o: CollectionValue,
+ firstElts: Value[],
+ firstLHKeys: ValueKey[],
+ secondElts: Value[],
+ secondLHKeys: ValueKey[]
+ ): void {
+ const deletedItems = [];
+ for (let i = 0; i < firstElts.length; i++) {
+ let notfound = true;
+ let j = 0;
+ while (notfound && j < secondElts.length) {
+ if (firstLHKeys[i] === secondLHKeys[j]) {
+ notfound = false;
+ const first = firstElts[i];
+ const second = secondElts[j];
+ if (first.str !== second.str) {
+ secondElts[i].setModified();
+ second.setModified();
+ if (first.constructor === second.constructor) {
+ // Only diff objects of identical types
+ first.diff(second);
+ }
+ }
+ }
+ j++;
+ }
+ if (notfound) {
+ deletedItems.push(firstElts[i]);
+ }
+ }
+ if (deletedItems.length > 0) {
+ o.addDeletedItems(deletedItems);
+ o.setModified();
+ }
+
+ for (let i = 0; i < secondElts.length; i++) {
+ const s = secondElts[i].str;
+ let notfound = true;
+ let j = 0;
+ while (notfound && j < firstElts.length) {
+ const f = firstElts[j].str;
+ if (f === s) {
+ notfound = false;
+ }
+ j++;
+ }
+ if (notfound) {
+ secondElts[i].setAdded();
+ }
+ }
+ }
}
/**
@@ -381,6 +446,33 @@ export class StructureValue extends CollectionValue {
formatKey(indent: string, value: Value): string {
return `${indent}${value.key}` + this.itemSep;
}
+
+ diff(other: Value): boolean {
+ /*
+ * RECORDS We mark a record element as added or deleted if its label
+ * does not appear in one of the elements of the other record. We
+ * mark the element as changed, and call setInnerDiffInfo on the
+ * elements' values if elements with the same label but different values
+ * appear in the two records.
+ */
+ if (!(other instanceof StructureValue)) {
+ return false;
+ }
+
+ const secondElts: StructureValue = (other as StructureValue);
+
+ const firstLHStrings: ValueKey[] = [];
+ for (let i = 0; i < this.items.length; i++) {
+ firstLHStrings[i] = this.items[i].key;
+ }
+ const secondLHStrings: ValueKey[] = [];
+ for (let i = 0; i < other.items.length; i++) {
+ secondLHStrings[i] = secondElts.items[i].key;
+ }
+
+ this.setElementArrayDiffInfo(this, other, this.items, firstLHStrings, secondElts.items, secondLHStrings);
+ return true;
+ }
}
/**
@@ -538,6 +630,15 @@ export function getStatusName(status: CheckStatus): string {
/**
* Recursively finds and marks all the changes between two collections.
*/
+export function findChangesOff(prev: CollectionValue, state: CollectionValue): boolean {
+ let i = 0;
+ while (i < prev.items.length && i < state.items.length) {
+ prev.items[i].diff(state.items[i]);
+ i++;
+ }
+ return true;
+}
+
export function findChanges(prev: CollectionValue, state: CollectionValue): boolean {
let pi = 0;
let si = 0;
from vscode-tlaplus.
@afonsonf Do you have plans to re-add the functionality that shows deleted set elements in the error trace view?
vscode-tlaplus/resources/check-result-view.js
Lines 334 to 336 in 0e16f40
A set will only be marked modified M
until the webview shows deleted set elements again.
from vscode-tlaplus.
Related Issues (20)
- Show model/spec name in VSCode status bar
- "Check Again" no-op if TLA+ debugger currently running HOT 1
- Check model with TLC is a no-op if there is no PlusCal in the file HOT 2
- Check Again should reuse the current window HOT 3
- Add Wiki documentation for TLC options HOT 3
- Using the extension with remote-ssh HOT 1
- "Output" tab on top of "Errors" tab
- Rename second column of states table from "Diameter" to "Depth" HOT 1
- The `tlaplus.tlaps.check-step` key-binding breaks VSCode's "go to line number" binding HOT 2
- Is there a way to add invariants as in the GUI? HOT 3
- Variables not working as Watch expression HOT 6
- LSP: Document annotations are sometimes lost. HOT 2
- LSP: TLAPS integration makes the IDE crash sometimes. HOT 1
- LSP: Proof step decorations look too distractive. HOT 1
- LSP: Add option to download the TLAPM/LSP.
- Merge "alygin.vscode-tlaplus" and "alygin.vscode-tlaplus-nightly" on Marketplace HOT 3
- Support ANSI escape sequence in trace explorer web view HOT 2
- LSP: Share module search paths between the TLAPS and SANY. HOT 4
- VSCode status panel stuck in computing initial states when using simulation mode HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from vscode-tlaplus.