iOS Live Activity: fit the lock screen with many threads

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 ("<hub>|<id>"): the reply's thread is read as the
 # hub's own id, so the spinner clears and the path joins that thread

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():
   {==}
 

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,34 +58,32 @@ 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) }
         }
         .contentShape(.rect)
     }
 }
 
-// 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: {

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}
 

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))

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