Keep the last tool call outside its group once it finishes
A call left its group only while it was running, so the moment a command ended it vanished behind "Called 3 tools" -- and a session that has run its last command and is composing its answer, or has finished the turn entirely, spends most of its time in exactly that state. What folds a call back into its run is therefore not finishing but being overtaken: anything arriving behind it, a reply included, makes it history. Standing outside the run is the call's place in the list as it is now rather than something recorded on the call, so it is asked of the list while grouping it, where the rest of that decision already lives. Checked with ktfmtFormat, compileDebugKotlin, testDebugUnitTest and lintDebug, and on the emulator against the sandbox: "/tools 3 1" settles as "Called 2 tools" with the third Bash card beneath it, and folds to "Called 3 tools" the moment the next reply lands.
This commit is contained in:
1 parent
036eb375aa
commit
1e52b2910c
4 files changed
+75
-42
No files matched your search
@@ -693,9 +693,9 @@ fun SessionScreen(
|
||||
}
|
||||
|
||||
// A call opened on its own stays open when it is folded into a group -- either because a second
|
||||
// call in the same run arrived, or because it finished and rejoined the run it was running
|
||||
// outside of. Until this, watching a Bash call and having the session make another one shut the
|
||||
// one being read and folded it behind "Called 2 tools".
|
||||
// call in the same run arrived, or because something landed behind the last call and it
|
||||
// rejoined the run it was standing outside of. Until this, watching a Bash call and having the
|
||||
// session make another one shut the one being read and folded it behind "Called 2 tools".
|
||||
//
|
||||
// Per call rather than per group, because a group outlives the calls joining it: considered at
|
||||
// the moment each call first lands inside one, and never again, so the reader who then shuts
|
||||
|
||||
Reference in new issue
Block a user