Fix diagram navigation and token highlighting

web/30-tabs.js

@@ -33,6 +33,7 @@ function addTab(o) {
   t.ed = makeEditor(t);
   t.ed.onInput = function () { onEdit(t); };
   t.ed.onCaret = updatePos;
+  t.ed.onPick = function () { if (t.kind === 'input') focusDiagramAt(t); };
   setEditorText(t.ed, o.text);
   $('editors').appendChild(t.ed.root);
   S.tabs.push(t);