Context
There were three navigations (the site menu, the Inside header, the docs bar) and two search boxes over two indexes, and docs search opened the first hit on Enter.
Decision
Every Inside page carries one top bar, written by bar() in scripts/inside_chrome.py. One index, /inside/search.json, merges the docs, the services and the map. The search box is a form that submits to /inside/search/, so Enter opens a results page. The deploy job rebuilds the index after the map refresh.
Consequences
A new Inside page must carry the marked bar block; python3 scripts/inside_chrome.py --check reports drift. The index is about 200 KB and loads when the box gets focus. See Top bar and search.