Messages never fold: only tool-call runs collapse; the "Worked for" turn fold hid the agent's messages between tool runs

LAWS.bend

@@ -1356,6 +1356,18 @@ law fold_default_live:
   for +live: Bool
   {FO.Fold.open("", live) == live : Bool}
 
+# a message is never folded away: it shows as itself wherever it sits
+law fold_roles_message_shown:
+  for +i: String
+  for +th: String
+  for +r: M.Role
+  for +x: String
+  for +a: Nat
+  for +t: List<&2, M.Entry>
+  for +info: Map<&2, String>
+  for +running: Bool
+  {List.head(&2, FO.Role, FO.Fold.roles(M.Msg{i, th, r, x, a} <> t, info, running)) == Some{FO.RShow{}} : Maybe<&2, FO.Role>}
+
 # a turn's work folds under its message: the message itself is never in
 # it, and while the turn runs its work stays open until shut by hand
 law work_message_shown:

PROOF.bend

@@ -4191,6 +4191,9 @@ def Laws.follow_alt_flips(s, p):
 def Laws.tailnet_link_token():
   {==}
 
+def Laws.fold_roles_message_shown(i, th, r, x, a, t, info, running):
+  {==}
+
 def Laws.work_message_shown(live, u, b, info, now):
   match live:
     case True{}:

src/core/fold.bend

@@ -13,11 +13,9 @@ import ./model.bend as M
 # client's info map), shut when they shut it ("0"), and otherwise open only
 # while it is the live one: the last thing in a thread whose turn runs.
 #
-# A turn folds the same way, one level up: what the agent did between a
-# user's message and its last reply shows as one row, "Worked for 2m 13s ·
-# 5m ago", open while the turn runs and shut once it is done
-# ("fold:work:<the user message's id>"). Inside it the tool runs fold as
-# before; the message and the reply are never in it (laws work_*).
+# Only tool calls fold: a turn's messages always show (law
+# fold_roles_message_shown). The turn fold below ("Worked for …", Work.*)
+# is no longer applied; it hid the agent's messages between tool runs.
 
 type Grp is Data:
   GOne{e: M.Entry}
@@ -403,6 +401,6 @@ def Fold.now(m: Map<&2, String>) -> Nat:
   M.Switch.num(Fold.user.k(Map.get(String, "", m, "clock")), 0n)
 
 # the roles of a thread's entries, with the client's info map and whether
-# its turn runs
+# its turn runs: tool runs fold, nothing else does
 def Fold.roles(+es: List<&2, M.Entry>, +info: Map<&2, String>, +running: Bool) -> List<&2, Role>:
-  Work.zip(Work.roles.go(Work.segs(es), info, running, Fold.now(info)), Fold.roles.go(Fold.groups(es), info, running))
+  Fold.roles.go(Fold.groups(es), info, running)

test/fold_test.bend

@@ -123,12 +123,10 @@ def main() -> IO(Unit):
     C.Check.str("user shut the live one", Show.roles(F.Fold.roles([tool("a", "x")], Map.set(&2, String, none(), "fold:a", "0"), True{})), "h(a|1 tool call · x|False) ")
     C.Check.str("ask", F.Fold.ask(True{}, "a") ++ " " ++ F.Fold.ask(False{}, "a"), "0a 1a")
     C.Check.str("took", M.Time.took(45n) ++ " " ++ M.Time.took(133n) ++ " " ++ M.Time.took(3900n), "45s 2m 13s 1h 5m")
-    C.Check.str("turn done: its work folds up to the last reply", Show.roles(F.Fold.roles(turn(), at(533n), False{})),
-      "s w(work:u|Worked for 2m 13s · 5m ago|False|h(a|2 tool calls · shell, edit|False)) i(False) i(False) i(False) s ")
-    C.Check.str("turn running: all of it open", Show.roles(F.Fold.roles(turn(), at(533n), True{})),
-      "s w(work:u|Working · started 7m ago|True|h(a|2 tool calls · shell, edit|False)) i(False) s h(c|1 tool call · read|False) s ")
-    C.Check.str("turn opened again", Show.roles(F.Fold.roles(turn(), Map.set(&2, String, at(240n), "fold:work:u", "1"), False{})),
-      "s w(work:u|Worked for 2m 13s · just now|True|h(a|2 tool calls · shell, edit|False)) i(False) s h(c|1 tool call · read|False) s ")
+    C.Check.str("turn done: its messages show, only tool runs fold", Show.roles(F.Fold.roles(turn(), at(533n), False{})),
+      "s h(a|2 tool calls · shell, edit|False) i(False) s h(c|1 tool call · read|False) s ")
+    C.Check.str("turn running: the last run open", Show.roles(F.Fold.roles([user("u", 0n), said("m", 1n), ran("a", "x", 2n)], at(533n), True{})),
+      "s s h(a|1 tool call · x|True) ")
     C.Check.str("turn with no reply: nothing folds", Show.roles(F.Fold.roles([user("u", 0n), ran("a", "x", 1n), err("e")], none(), False{})),
       "s h(a|1 tool call · x|False) s ")
     C.Check.str("turn answered at once: nothing folds", Show.roles(F.Fold.roles([user("u", 0n), said("m", 1n)], none(), False{})), "s s ")