Skip to content
This repository was archived by the owner on Nov 11, 2022. It is now read-only.

Tighten up edit input activeness check in spec #15

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Tighten up edit input activeness check in spec #15

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions case-studies/todomvc.strom
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ let ~changeFilter =
});

let ~setSameFilter =
editInput == null &&
unchanged([
selectedFilter,
newTodoInput.pendingText,
Expand All @@ -104,7 +105,7 @@ let ~addNew =
// Blank todo items cannot be created.
trimmed != ""
// Creating an item clears the input and always enabled one of the filters.
&& newTodoInput.pendingText becomes "" && selectedFilter does not become null
&& newTodoInput.pendingText becomes "" // && selectedFilter does not become null
// Pressing return is the only way to create a todo item.
&& nextT (contains(keyPress!(keys.return), happened))
&& (match selectedFilter {
Expand Down Expand Up @@ -194,7 +195,7 @@ let ~toggleAll =
});

let ~startEditing =
(numInEditMode == 0) ~> (numInEditMode == 1 && editInput.active)
((numInEditMode == 0) ~> (numInEditMode == 1 && editInput.active))
&& unchanged([
newTodoInput.pendingText,
selectedFilter,
Expand Down Expand Up @@ -245,8 +246,10 @@ let ~enterEditMode =
);

let ~editModeTransition =
(numInEditMode == 1 ~> numInEditMode == 1)
|| (numInEditMode == 1 ~> numInEditMode == 0);
editInput != null
&& editInput.active
&& ((numInEditMode == 1 ~> numInEditMode == 1)
|| (numInEditMode == 1 ~> numInEditMode == 0));

// Global Invariants

Expand Down