Phones: instant open for bots, the uberbot, rooms and threads; the person's taps ahead of streaming

LAWS.bend

@@ -7002,3 +7002,34 @@ law agy_google_warns:
 law agy_callback_needs_signin:
   for b: String
   {AGY.Agy.callback.ok("", b) == False{} : Bool}
+
+# ios-snappy: nav
+# The bot row's nav, qualified by its hub, is the same qualified thread
+# sel the opened screen carries. This example has an arbitrary t-prefixed
+# thread id; the general law below covers all untagged nonempty threads.
+# Room and reported bot keys stay local.
+law mnav_bot_sel:
+  for +hub: String
+  for +id: String
+  for +tail: String
+  {Hb.Hubs.nav.bot(hub, BU.BRow{id, "", "t" ++ tail, 0n, "idle", "", False{}, False{}, "", ""}) == Hb.Hubs.id(hub, "t" ++ tail) : String}
+
+law mnav_room_local:
+  for +hub: String
+  for +id: String
+  {Hb.Hubs.nav.qual(hub, "@room:" ++ id) == "@room:" ++ id : String}
+
+law mnav_remote_local:
+  for +hub: String
+  for +id: String
+  {Hb.Hubs.nav.qual(hub, "@remote:" ++ id) == "@remote:" ++ id : String}
+
+# Every valid bot thread qualifies exactly like the opened screen's sel.
+# The reserved room/remote prefixes name other destination kinds.
+law mnav_bot_thread:
+  for +hub: String
+  for +id: String
+  for +thread: String
+  for some: {String.is_empty(thread) == False{} : Bool}
+  for own: {Hb.Hubs.nav.tag(thread) == False{} : Bool}
+  {Hb.Hubs.nav.bot(hub, BU.BRow{id, "", thread, 0n, "idle", "", False{}, False{}, "", ""}) == Hb.Hubs.id(hub, thread) : String}

PROOF.bend

@@ -45,6 +45,7 @@ import ./src/gfx/face.bend as FA
 import ./src/core/glb.bend as G
 import ./src/mobile/picker.bend as MP
 import ./src/mobile/hubs.bend as Hb
+import ./src/mobile/bots.bend as MBN
 import ./src/core/space.bend as SPC
 import ./src/core/client.bend as U
 import ./src/core/menu.bend as MN
@@ -8453,3 +8454,18 @@ def Laws.agy_google_warns():
 def Laws.agy_callback_needs_signin(b):
   {==}
 
+
+# ios-snappy: nav
+def Laws.mnav_bot_sel(hub, id, tail):
+  {==}
+
+def Laws.mnav_room_local(hub, id):
+  {==}
+
+def Laws.mnav_remote_local(hub, id):
+  {==}
+
+def Laws.mnav_bot_thread(hub, id, thread, some, own):
+  %Equal.sym(Bool, String.is_empty(thread), False{}, some) : {Hb.Hubs.nav.qual(hub, MBN.MBots.nav.k(_, id, thread)) == Hb.Hubs.id(hub, thread) : String}
+  %Equal.sym(Bool, Hb.Hubs.nav.tag(thread), False{}, own) : {Bool.pick(String, _, thread, Hb.Hubs.id(hub, thread)) == Hb.Hubs.id(hub, thread) : String}
+  {==}

mobile/android/app/src/main/java/dev/backplane/mobile/AppModel.kt

@@ -10,6 +10,13 @@ class AppModel(app: Application) : AndroidViewModel(app) {
 
     val links get() = core.links
     val screen get() = core.screen
+    val opening get() = core.opening
+    val leaving get() = core.leaving
+    val seenThreads get() = core.seenThreads
+    val seenBots get() = core.seenBots
+    val seenPages get() = core.seenPages
+    fun open(nav: String, action: String, value: String, title: String, cat: String = "", kind: String = "thread") = core.open(nav, action, value, title, cat, kind)
+    fun back() = core.back()
     // the card and the plane to draw: the screen's, else the last it carried
     fun uber(s: Screen): UberCard? = if (s.plane != null) s.uber else if (s.uber != null) core.lastUber ?: s.uber else null
     fun plane(s: Screen): PlaneModel? = s.plane ?: if (s.uber != null) core.lastPlane else null

mobile/android/app/src/main/java/dev/backplane/mobile/Bots.kt

@@ -152,15 +152,15 @@ fun LazyListScope.botsSection(m: AppModel, s: Screen) {
             },
             leadingContent = { BotCat(m, b.cat, 40.dp) },
             modifier = Modifier.alpha(if (b.mood == "away") 0.5f else 1f)
-                .clickable { m.act(b.act, b.id) },
+                .clickable { m.open(b.nav, b.act, b.id, b.name, b.cat, if (b.remote) "remote" else "bot") },
         )
     }
     items(s.rooms, key = { "r:" + it.id }) { r ->
         ListItem(
             headlineContent = { Text(r.name, maxLines = 1, overflow = TextOverflow.Ellipsis) },
             supportingContent = { Text(listOf("${r.members}", r.machine).filter { it.isNotEmpty() }.joinToString(" · ")) },
             leadingContent = { Box(Modifier.size(40.dp), contentAlignment = Alignment.Center) { Icon(Icons.Filled.Forum, null) } },
-            modifier = Modifier.clickable { m.act("room", r.id) },
+            modifier = Modifier.clickable { m.open(r.nav, "room", r.id, r.name, kind = "room") },
         )
     }
 }
@@ -272,7 +272,7 @@ private fun BotScreen(m: AppModel, s: Screen, b: BotView) {
         Column {
             TopAppBar(
                 title = { Text(b.name, maxLines = 1, overflow = TextOverflow.Ellipsis) },
-                navigationIcon = { IconButton(onClick = { m.act("select", "") }) { Icon(Icons.AutoMirrored.Filled.ArrowBack, "Back") } },
+                navigationIcon = { IconButton(onClick = { m.back() }) { Icon(Icons.AutoMirrored.Filled.ArrowBack, "Back") } },
             )
             BotTabs(m, b)
         }
@@ -582,7 +582,7 @@ private fun TalkScreen(m: AppModel, b: BotView, field: String, send: String) {
                                 color = MaterialTheme.colorScheme.outline, maxLines = 1, overflow = TextOverflow.Ellipsis)
                         }
                     },
-                    navigationIcon = { IconButton(onClick = { m.act("select", "") }) { Icon(Icons.AutoMirrored.Filled.ArrowBack, "Back") } },
+                    navigationIcon = { IconButton(onClick = { m.back() }) { Icon(Icons.AutoMirrored.Filled.ArrowBack, "Back") } },
                     actions = {
                         if (b.kind == "room") Box {
                             IconButton(onClick = { menu = true }) { Icon(Icons.Filled.MoreVert, "More") }

mobile/android/app/src/main/java/dev/backplane/mobile/Core.kt

@@ -48,6 +48,52 @@ class Core(private val app: Application) : Application.ActivityLifecycleCallback
     var lastUber by mutableStateOf<UberCard?>(null)
     var lastPlane by mutableStateOf<PlaneModel?>(null)
         private set
+    data class Opening(val nav: String, val title: String, val cat: String, val kind: String)
+    var opening by mutableStateOf<Opening?>(null)
+        private set
+    var leaving by mutableStateOf(false)
+        private set
+    private var pushed = Long.MIN_VALUE
+    private var tapAt = 0L
+    private var firstMs = 0L
+    val seenThreads = mutableStateMapOf<String, ThreadView>()
+    val seenBots = mutableStateMapOf<String, BotView>()
+    val seenPages = mutableStateMapOf<String, Screen>()
+    private val threadOrder = java.util.ArrayDeque<String>()
+    private val botOrder = java.util.ArrayDeque<String>()
+    private val pageOrder = java.util.ArrayDeque<String>()
+
+    companion object {
+        fun nav(s: Screen): String = s.bot?.let { if (it.kind != "bot") "@${it.kind}:${it.id}" else s.sel } ?: s.sel
+    }
+
+    fun open(nav: String, action: String, value: String, title: String, cat: String = "", kind: String = "thread") {
+        val now = android.os.SystemClock.elapsedRealtime()
+        if (nav.isEmpty() || opening?.nav == nav || (!leaving && screen?.let { Core.nav(it) } == nav) ||
+            (pushed != Long.MIN_VALUE && now - pushed < 350)) return
+        pushed = now
+        tapAt = now
+        leaving = false
+        val rig = cat.ifEmpty { screen?.bots?.firstOrNull { it.nav == nav }?.cat ?: screen?.uber?.takeIf { it.nav == nav }?.cat ?: "" }
+        opening = Opening(nav, title, rig, kind)
+        firstMs = android.os.SystemClock.elapsedRealtime() - tapAt
+        dispatch(action, value)
+    }
+
+    fun back() {
+        opening = null
+        leaving = true
+        tapAt = 0L
+        act("select", "")
+    }
+
+    private fun <T> remember(nav: String, value: T, map: MutableMap<String, T>, order: java.util.ArrayDeque<String>) {
+        map[nav] = value
+        order.remove(nav)
+        order.addLast(nav)
+        if (order.size > 24) map.remove(order.removeFirst())
+    }
+
     // the composer's text, owned here so typing never waits on Bend
     var composer by mutableStateOf("")
         private set
@@ -73,6 +119,7 @@ class Core(private val app: Application) : Application.ActivityLifecycleCallback
     val foreground get() = started > 0
 
     init {
+        engine.onFlush = { out -> scope.launch { apply(out) } }
         app.registerActivityLifecycleCallbacks(this)
         val t0 = android.os.SystemClock.elapsedRealtime()
         fun since() = android.os.SystemClock.elapsedRealtime() - t0
@@ -191,7 +238,18 @@ class Core(private val app: Application) : Application.ActivityLifecycleCallback
         ).also { it.start() }
     }
 
+    private fun dispatch(action: String, value: String) {
+        scope.launch { apply(engine.act(action, value)) }
+    }
+
     fun act(action: String, value: String = "") {
+        // a page on its way takes no other action (a cached page is inert);
+        // given up after 3 s, so a page that never comes never freezes the app
+        if (opening != null) {
+            if (android.os.SystemClock.elapsedRealtime() - pushed < 3000) return
+            opening = null
+            tapAt = 0L
+        }
         // a web address a settings row offers (Antigravity's sign-in):
         // opened in the browser here, never sent to the engine
         if (action == "open-url") {
@@ -200,7 +258,7 @@ class Core(private val app: Application) : Application.ActivityLifecycleCallback
                 runCatching { app.startActivity(android.content.Intent(android.content.Intent.ACTION_VIEW, u).addFlags(android.content.Intent.FLAG_ACTIVITY_NEW_TASK)) }
             return
         }
-        scope.launch { apply(engine.act(action, value)) }
+        dispatch(action, value)
     }
 
     // an action whose effect shows only with what the hub answers (a key
@@ -298,6 +356,18 @@ class Core(private val app: Application) : Application.ActivityLifecycleCallback
             if (typing == 0) composer = next.thread?.draft ?: ""
             val was = screen?.sel
             screen = next
+            val nav = nav(next)
+            if (nav.isNotEmpty()) {
+                next.thread?.let { remember(nav, it, seenThreads, threadOrder) }
+                next.bot?.let { remember(nav, it, seenBots, botOrder) }
+                remember(nav, next.copy(projects = emptyList(), bots = emptyList(), rooms = emptyList()), seenPages, pageOrder)
+            }
+            if (opening?.nav == nav) {
+                android.util.Log.i("Backplane", "tap $nav first $firstMs ms full ${android.os.SystemClock.elapsedRealtime() - tapAt} ms")
+                opening = null
+                tapAt = 0L
+            }
+            if (leaving && nav.isEmpty()) leaving = false
             if (next.uber == null) { lastUber = null; lastPlane = null }
             else if (next.plane != null) { lastUber = next.uber; lastPlane = next.plane }
             if (next.hub != shownHub) {