diff --git a/LAWS.bend b/LAWS.bend index 774c7a64b7..21960116f5 100644 --- a/LAWS.bend +++ b/LAWS.bend @@ -4858,6 +4858,12 @@ law island_unheard_late: law island_unheard_recent: {Nt.Note.heard.in(False{}, 12n, 5n, 10n) == True{} : Bool} +# a Live Activity counts every thread but lists only the first few, so it +# fits the lock screen and a push (Notice.island.max) +law island_lines_capped: + {J.Json.show(Nt.Note.island.k.named([J.Json.nat(1n), J.Json.nat(2n), J.Json.nat(3n), J.Json.nat(4n), J.Json.nat(5n)], "")) + == "{\"running\":5,\"headline\":\"5 agents working\",\"lines\":[1,2,3]}" : String} + # a phone's upload ends under the thread it started in, though the phone # named it with its hub ("|"): the reply's thread is read as the # hub's own id, so the spinner clears and the path joins that thread diff --git a/PROOF.bend b/PROOF.bend index 73333b0d26..44411e6112 100644 --- a/PROOF.bend +++ b/PROOF.bend @@ -6755,6 +6755,9 @@ def Laws.island_unheard_late(): def Laws.island_unheard_recent(): {==} +def Laws.island_lines_capped(): + {==} + def Laws.upload_thread_local(): {==} diff --git a/mobile/ios/Island/IslandWidget.swift b/mobile/ios/Island/IslandWidget.swift index 58c8b59fa5..6f59215bba 100644 --- a/mobile/ios/Island/IslandWidget.swift +++ b/mobile/ios/Island/IslandWidget.swift @@ -34,13 +34,14 @@ private func tap(_ s: IslandAttributes.ContentState) -> URL? { s.lines.count == 1 ? link(s.lines[0].thread) : link("", pick: true) } -// each thread its own row, a tap on it opens that thread +// each thread its own row, a tap on it opens that thread. The hub sends +// only the first few (notice.bend's Notice.island.max) and counts the rest private struct Lines: View { let lines: [IslandAttributes.Line] let titles: Bool var body: some View { - VStack(alignment: .leading, spacing: 6) { + VStack(alignment: .leading, spacing: 4) { ForEach(lines, id: \.thread) { l in if let u = link(l.thread) { Link(destination: u) { Row(line: l, title: titles) } @@ -57,12 +58,14 @@ private struct Row: View { let line: IslandAttributes.Line let title: Bool + // one line a thread, so several fit the lock screen's 160 points var body: some View { HStack(spacing: 6) { - VStack(alignment: .leading, spacing: 1) { - if title { Text(line.title).font(.caption.weight(.semibold)).lineLimit(1) } - Text(line.doing).font(.caption.monospaced()).foregroundStyle(.secondary).lineLimit(1) + if title { + Text(line.title).font(.caption.weight(.semibold)).lineLimit(1) + .frame(maxWidth: 150, alignment: .leading) } + Text(line.doing).font(.caption.monospaced()).foregroundStyle(.secondary).lineLimit(1) Spacer(minLength: 4) if title { Image(systemName: "chevron.right").font(.caption2).foregroundStyle(.tertiary) } } @@ -70,21 +73,17 @@ private struct Row: View { } } -// what is not shown: "+ N more" -private struct More: View { - let n: Int - - var body: some View { - if n > 0 { Text("+ \(n) more").font(.caption2).foregroundStyle(.secondary) } - } -} - -// no word from the hubs for hours: this may no longer be so (open the app) -private struct Stale: View { +// one line under the rows: what is not shown ("+ N more"), and, with no +// word from the hubs for hours, that this may no longer be so +private struct Foot: View { + let more: Int let stale: Bool var body: some View { - if stale { Text("Not updated lately: open Backplane").font(.caption2).foregroundStyle(.secondary) } + let words = (more > 0 ? ["+ \(more) more"] : []) + (stale ? ["Not updated lately: open Backplane"] : []) + if !words.isEmpty { + Text(words.joined(separator: " · ")).font(.caption2).foregroundStyle(.secondary).lineLimit(1) + } } } @@ -99,9 +98,8 @@ struct IslandWidget: Widget { Spacer() if s.running > 1 { Text("\(s.running)").font(.headline.monospacedDigit()) } } - Lines(lines: Array(s.lines.prefix(4)), titles: s.running > 1) - More(n: s.lines.count - 4) - Stale(stale: ctx.isStale) + Lines(lines: s.lines, titles: s.running > 1) + Foot(more: s.running - s.lines.count, stale: ctx.isStale) } .opacity(ctx.isStale ? 0.5 : 1) .padding() @@ -120,9 +118,8 @@ struct IslandWidget: Widget { } DynamicIslandExpandedRegion(.bottom) { VStack(alignment: .leading, spacing: 4) { - Lines(lines: Array(s.lines.prefix(4)), titles: s.running > 1) - More(n: s.lines.count - 4) - Stale(stale: ctx.isStale) + Lines(lines: s.lines, titles: s.running > 1) + Foot(more: s.running - s.lines.count, stale: ctx.isStale) } } } compactLeading: { diff --git a/src/core/notice.bend b/src/core/notice.bend index 6b43f84f43..0464d576c1 100644 --- a/src/core/notice.bend +++ b/src/core/notice.bend @@ -32,6 +32,13 @@ import ./far.bend as FR def Notice.window() -> Nat: 300n +# how many threads a Live Activity lists (the rest are "+ N more" from its +# running count): its lock-screen view is at most 160 points tall, and a +# hub's APNs push of it at most 4 KB, so every one of many never fits (law +# island_lines_capped) +def Notice.island.max() -> Nat: + 3n + type Notice is Data: Notice{kind: String, key: String} diff --git a/src/mobile/notify.bend b/src/mobile/notify.bend index 488a41510a..b4803af8f8 100644 --- a/src/mobile/notify.bend +++ b/src/mobile/notify.bend @@ -234,10 +234,12 @@ def Note.island.k(+ls: List<&2, J.Json>) -> J.Json: def Note.named(+h: String, +name: String) -> String: Bool.pick(String, String.is_empty(name), h, h ++ " · " ++ name) +# (a Live Activity's: every thread counted, the first NO.Notice.island.max() +# listed) def Note.island.k.named(+ls: List<&2, J.Json>, +name: String) -> J.Json: J.Json.obj([J.KV{"running", J.Json.nat(List.length(&2, J.Json, ls))}, J.KV{"headline", J.Json.str(Note.named(Note.headline(List.length(&2, J.Json, ls), Note.first(ls)), name))}, - J.KV{"lines", J.Json.arr(ls)}]) + J.KV{"lines", J.Json.arr(List.take(&2, J.Json, ls, NO.Notice.island.max()))}]) def Note.island(ts: List<&2, M.Thread>, +es: List<&2, M.Entry>) -> J.Json: Note.island.k(Note.lines(ts, es)) diff --git a/src/server/push.bend b/src/server/push.bend index 073acad1bf..faeed77a6d 100644 --- a/src/server/push.bend +++ b/src/server/push.bend @@ -252,11 +252,12 @@ def Island.headline(n: Nat, +title: String) -> String: case 1n+1n+p: Nat.show(2n+p) ++ " agents working" -# ActivityAttributes.ContentState: {running, headline, lines} +# ActivityAttributes.ContentState: {running, headline, lines}, every thread +# counted, the first NO.Notice.island.max() listed def Island.state(+ts: List<&2, M.Thread>) -> J.Json: J.Json.obj([J.KV{"running", J.Num{Nat.show(List.length(&2, M.Thread, ts))}}, J.KV{"headline", J.Str{Island.headline(List.length(&2, M.Thread, ts), Island.first(ts))}}, - J.KV{"lines", J.Json.arr(Island.lines(ts))}]) + J.KV{"lines", J.Json.arr(Island.lines(List.take(&2, M.Thread, ts, NO.Notice.island.max())))}]) # an ended island goes at once: one left on the lock screen read "All # agents idle" beside the next one started