Implement staleness validation and skip-with-banner

Every crossing validates its expectations before writing: each step
carries per-item HistoryExpectations — folder, effective ancestor-walked
liveness, and exactly the fields the gesture set — and a mismatch pops
the step, posts the signpost ('Undo skipped — Fix login changed outside
Lanework'), and falls through to the next. Validation reads disk, not
the in-memory snapshot: the snapshot is by construction one reload
behind every app write, so a rapid second undo would false-skip against
the pre-state — disk is what current can honestly mean at press time.
Stale and failed part ways: a stale step is one the board moved past,
so dropping it loses nothing; a failed one is refused by a usually
momentary condition, so it stays put and the crossing stops with only
performWrite's own error row — which forced the provider off
NSUndoManager onto two plain arrays, since a popped group cannot be put
back. The read-only lock disables Undo/Redo through the adapter while
the stack survives to resume on clear. Delete and restore validate
presence alone — a machine timestamp is not a decision — and a
malformed field matches nothing, since it is a shape the app never
writes.

Claude-Session: https://claude.ai/code/session_01SR4XGjmBE16ZUYWpfFHXwY
This commit is contained in:
2026-07-28 14:54:42 -04:00
parent 2148ebb379
commit 50669489cb
10 changed files with 1333 additions and 149 deletions
+115 -17
View File
@@ -23,9 +23,19 @@ import os
/// Nothing a step closes over is read from the snapshot at crossing time: every closure below
/// captures ids, folder URLs, orders, titles, style values and body bytes as **values**, computed
/// from the pre-write snapshot the store was holding when the gesture ran. That is what makes a step
/// meaningful minutes later, after any number of reloads, and it is what the next milestone's
/// field-level staleness predicate compares against each step already carries both sides of its
/// write (13 Rules staleness validation).
/// meaningful minutes later, after any number of reloads, and it is what the **field-level staleness
/// predicate** compares against each step carries both sides of its write (13 Rules staleness
/// validation).
///
/// ### Every step declares what its write left behind
///
/// Beside the two closures, each registration below hands the funnel two `[HistoryExpectation]`
/// lists: what the board must look like for the undo to be safe (the state the *forward* write left),
/// and what it must look like for the redo to be safe (the state the *undo* leaves). One entry per
/// item the gesture touched, naming that item's folder, whether it should be there and live, and the
/// fields the write actually set "extend the registration to carry whatever the predicate needs, no
/// more". A field this gesture never wrote is never listed, which is what makes a foreign edit
/// elsewhere another card, another field of the same card leave the step alone.
@MainActor
extension BoardStore {
@@ -39,11 +49,20 @@ extension BoardStore {
/// weak one this method installs: a stack outliving its session must not be the reason a board
/// stays in memory.
///
/// **A step that could not write answers `.skipped`.** `HistoryStepOutcome` has two cases and the
/// honest reading of a failed inverse is the second one nothing landed, so nothing goes on the
/// opposite stack and `performWrite` has already posted the banner that says why. The read-only
/// lock, the other way a write is refused here, cannot reach this path in practice: a lock
/// disables Undo and Redo with the rest of the mutating commands (13 Rules locks).
/// `subject` is what the **skip banner** quotes: the item's title where the step names exactly
/// one titled item, and otherwise `nil`, which falls back to the step's own 06 phrase. That is
/// two readings of one sentence rather than two sentences 13's own example is an item ("Undo
/// skipped 'Fix login' changed outside Lanework") and a batch has no single item to name, so it
/// says what it is instead ("Undo skipped 'Move 3 Cards' changed outside Lanework"). An
/// untitled item takes the phrase too: "Untitled" is a rendering, never a value (03-board-ui.md
/// § Card face).
///
/// **A failed inverse answers `.failed`, a stale one `.skipped`** the distinction the stack
/// depends on (`HistoryStepOutcome`): a stale step is dropped and Z falls through, a failed one
/// stays put with `performWrite`'s error banner already standing. The read-only lock reaches this
/// path only from a direct call the adapter disables Undo and Redo under it
/// (`BoardUndoManager`, 13 Rules locks) and is a refusal rather than a staleness, so it too
/// leaves the stack where it is: the lock clears, the stack resumes.
///
/// The seam is spelled with an **untyped** `throws`, deliberately and at a cost worth recording:
/// every inverse below is made of `BoardWriter` calls and throws nothing but `BoardWriteError`,
@@ -54,25 +73,48 @@ extension BoardStore {
/// than swallows the case that cannot happen.
func registerStep(
_ name: String,
subject: String? = nil,
undoExpects: [HistoryExpectation],
redoExpects: [HistoryExpectation],
undo: @escaping @MainActor (BoardStore) throws -> Void,
redo: @escaping @MainActor (BoardStore) throws -> Void
) {
guard let history else { return }
let named = subject ?? name
history.register(HistoryStep(
name: name,
undo: { [weak self] in BoardStore.cross(self, undo) },
redo: { [weak self] in BoardStore.cross(self, redo) }
undo: { [weak self] direction in
BoardStore.cross(self, direction, named, undoExpects, undo)
},
redo: { [weak self] direction in
BoardStore.cross(self, direction, named, redoExpects, redo)
}
))
}
/// Runs one side of a step as an ordinary bracketed write.
/// Validates one side of a step against disk, then runs it as an ordinary bracketed write.
///
/// The order is the whole rule: **nothing is written until every target still holds what this
/// step left there** (13 Rules staleness validation, "Never apply a stale inverse on top of
/// someone else's newer write"). A stale target posts the info-tone row that explains the skip and
/// answers `.skipped`, which pops the step and falls the crossing through to the next one down.
private static func cross(
_ store: BoardStore?,
_ direction: HistoryDirection,
_ subject: String,
_ expectations: [HistoryExpectation],
_ write: @MainActor (BoardStore) throws -> Void
) -> HistoryStepOutcome {
// The board went away under its own stack a session torn down between the registration and
// the Z. Nothing to write to, so nothing ran.
guard let store else { return .skipped }
// the Z. There is nothing to write to and nothing to say it on, and a step whose board is
// gone is not one to pop: the stack is about to be cleared with the session anyway.
guard let store else { return .failed }
guard HistoryStaleness.isCurrent(expectations, under: store.rootURL) else {
store.banners.postSkippedStep(direction, subject: subject)
return .skipped
}
var foreign: (any Error)?
let landed: Void? = try? store.performWrite { () throws(BoardWriteError) -> Void in
do {
@@ -87,9 +129,11 @@ extension BoardStore {
}
if let foreign {
historyLogger.error("an inverse threw something that is not a write error: \(String(describing: foreign), privacy: .public)")
return .skipped
return .failed
}
return landed == nil ? .skipped : .applied
// `nil` is either the Writer's `BoardWriteError` (bannered on the way past) or the read-only
// lock's refusal (the lock row is already standing). Both are failures, never staleness.
return landed == nil ? .failed : .applied
}
private static let historyLogger = Logger(subsystem: "dev.rzen.indie.Kanban", category: "history")
@@ -124,10 +168,22 @@ extension BoardStore {
/// hand, a foreign edit goes with the folder and does not come back on redo. That follows from
/// 13's own two rulings (remove the folder; attachment operations register nothing in v1) rather
/// than from anything decided here.
func registerCreation(_ items: [CreatedItem], kind: HistoryPhrase.Kind) {
///
/// **Its staleness predicate is existence and liveness, and deliberately nothing else** (13:
/// "existence/liveness for create/delete/restore steps"). A create's after-value *is* the item's
/// being there, so the undo validates that the folders are still there and still live and the
/// redo that they are still gone. The same honest edge follows: a foreign *edit* inside a created
/// card does not stop Z from removing it, because the create never wrote that field while a
/// foreign *delete* does, since the trash row the user is looking at is not this step's to purge.
func registerCreation(_ items: [CreatedItem], kind: HistoryPhrase.Kind, subject: String? = nil) {
guard !items.isEmpty else { return }
let operation: WriteOperation = kind == .lane ? .createLane : .createCard
registerStep(HistoryPhrase.name(.add, kind: kind, count: items.count)) { _ in
registerStep(
HistoryPhrase.name(.add, kind: kind, count: items.count),
subject: subject,
undoExpects: items.map { .live($0.folder) },
redoExpects: items.map { .absent($0.folder) }
) { _ in
// Reversed, so a lane and a card created by one gesture unwind child-first the same
// order they were made in, read backwards.
for item in items.reversed() {
@@ -170,6 +226,48 @@ extension BoardStore {
}
}
/// The style fields a gesture actually set **one entry per dimension it did not `.keep`**, so a
/// step that only chose a colour never validates the symbol beside it.
///
/// `.remove` is spelled as `nil`, which is the after-value the None well leaves: the key is gone,
/// and the item renders the level's default (03-board-ui.md § Styling Controls).
static func styledFields(background: StyleChange, icon: StyleChange) -> [ExpectedField] {
field(background, as: ExpectedField.background) + field(icon, as: ExpectedField.icon)
}
/// The same dimensions, holding the values the *inverse* restores what the redo half validates
/// against once Z has run.
///
/// The prior is read as `FieldValue.value`, which is `nil` for a missing key **and** for a
/// malformed one, exactly matching `restore(_:to:in:)`: a malformed prior reads as a removal, so
/// the state the undo leaves is an absent key either way.
static func restoredStyleFields(
background: StyleChange,
priorBackground: FieldValue<String>,
icon: StyleChange,
priorIcon: FieldValue<String>
) -> [ExpectedField] {
var fields: [ExpectedField] = []
if background != .keep {
fields.append(.background(priorBackground.value))
}
if icon != .keep {
fields.append(.icon(priorIcon.value))
}
return fields
}
private static func field(
_ change: StyleChange,
as make: (String?) -> ExpectedField
) -> [ExpectedField] {
switch change {
case .keep: []
case let .set(value): [make(value)]
case .remove: [make(nil)]
}
}
/// Puts a lane's `width` back the integer it held, or no key at all.
///
/// Note the asymmetry with the forward write, which removes the key at one unit (the