HAXY

▄▄ ▀▀▀▄ ▄▄ ▀▀▀▀▀▄ ▄▀▀▀▀ ▀▀▀▀▀▀ ▄▀▀▀▀▀▀ ▀▀▀▀▀▀ ▀ ▀ ▄▀▀▀▀▀▀ ▀▀▀▀▀▀ ▄▀ ▄▀ ▄▀▀▀▀▀▀▀▀ ▀▀▀▄▄ ▀▀▀▀▀▀ ▀▀ ▀▄▀▀ ▄▀ ▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▄ ▀▀▀▀▀▄ ▄▀▀▀▀▀▀▀ ▄ ▄▀▄▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▄ ▄▀▀▀▀▀▀▀▀▀▀▄ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▄ ▀ ▀▀▀▀▀▀ ▄▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀ ▄▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▄▀▀▀▀▀▀▀▀▀▀▀▀▀▀▄ ▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▄ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▄▄▄▀▀▀▀▄▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▄▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▄ ▀▀▀▀▀▀▀▀▀▀▀▀▀▄▀▀▀▀▀▀▀▀▀▀▄ ▄▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▄▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▄▄ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▄▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀ ▀▀▀▀▀▀▀▀▄ ▀▀▀ ▀▀▀▀▀▀▀▀ ▀▀▀ ▀▀▀ ▀▀▀▀▀ ▀▀ ▀▀▀▀▀▀ ▀▀▀▄▀▄ ▄▄▄▀▀ ▀▀▀▀▀▀ ▀▀▄▀▀▀▀▀▀▀ ▀▀▀▀▀▄▀▀▀▀▀ ▀▀▀▀▀▄ ▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▄▀ ▄▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀▀▀▀▀▀▀▀▀▀ ▀▀▀ ▀

╭ changed ─────────────╮ │src/ui/Fork/Header.zig│ ╰──────────────────────╯ ╭────────────────────────────────────────────────────────────╮ │40 scroll: wgt.Scroll(ui.Widget), │ │41 tab_ids: std.AutoArrayHashMapUnmanaged(usize, void),│ │42 tabs_id: usize, │ │43 + gap_id: usize, │ │44 first_group_width: usize, │ │45 session: *ui.Session, │ │46 │ ╰────────────────────────────────────────────────────────────╯ ╭──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╮ │168 const tabs_id = tabs_box.getFocus().id; │ │169 try box.children.put(allocator, title_id, .{ .widget = .{ .box = title_box }, .rect = null, .min_size = null }); │ │170 title_box_owned = true; │ │171 + // a blank row between the title and the tabs, shown only when they wrap │ │172 + const gap_id = blk: { │ │173 + var gap = try wgt.Text.init(allocator, " "); │ │174 + errdefer gap.deinit(allocator); │ │175 + const id = gap.getFocus().id; │ │176 + try box.children.put(allocator, id, .{ .widget = .{ .text = gap }, .rect = null, .min_size = null, .hidden = true });│ │177 + break :blk id; │ │178 + }; │ │179 try box.children.put(allocator, tabs_id, .{ .widget = .{ .box = tabs_box }, .rect = null, .min_size = null }); │ │180 tabs_box_owned = true; │ │181 box.getFocus().child_id = tabs_id; │ ╰──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╯ ╭───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╮ │184 .scroll = try wgt.Scroll(ui.Widget).init(allocator, .{ .box = box }, .{ .direction = .horiz, .show_bar = false, .web_native = !session.is_terminal }),│ │185 .tab_ids = tab_ids, │ │186 .tabs_id = tabs_id, │ │187 + .gap_id = gap_id, │ │188 .first_group_width = first_group_width, │ │189 .session = session, │ │190 }; │ ╰───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╯ ╭─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╮ │224 const wrap = if (content_width) |width| self.first_group_width + back_width + tabs_width > width else false;│ │225 box.options.direction = if (wrap) .vert else .horiz; │ │226 tabs_child.min_size = if (wrap) .{ .width = content_width, .height = null } else null; │ │227 + (box.children.getPtr(self.gap_id) orelse unreachable).hidden = !wrap; │ │228 │ │229 var scroll_constraint = constraint; │ │230 scroll_constraint.min_size.width = viewport_width; │ ╰─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╯ ╭ changed ─────────────╮ │src/ui/Home/Header.zig│ ╰──────────────────────╯ ╭──────────────────────────────────────────────────────────────────────────────────────────────────╮ │28 pub const View = struct { │ │29 scroll: wgt.Scroll(ui.Widget), │ │30 tab_ids: std.AutoArrayHashMapUnmanaged(usize, void), │ │31 + tabs_id: usize, │ │32 + gap_id: usize, │ │33 + first_group_width: usize, │ │34 session: *ui.Session, │ │35 │ │36 pub fn init(allocator: std.mem.Allocator, data: *const Self, session: *ui.Session) !View {│ ╰──────────────────────────────────────────────────────────────────────────────────────────────────╯ ╭─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╮ │37 var box = try wgt.Box(ui.Widget).init(allocator, .{ .border_style = .hidden, .rounded_corners = true, .direction = .horiz });│ │38 errdefer box.deinit(allocator); │ │39 │ │40 + var title_box = try wgt.Box(ui.Widget).init(allocator, .{ .border_style = null, .direction = .horiz }); │ │41 + var title_box_owned = false; │ │42 + errdefer if (!title_box_owned) title_box.deinit(allocator); │ │43 + │ │44 + var tabs_box = try wgt.Box(ui.Widget).init(allocator, .{ .border_style = null, .direction = .horiz }); │ │45 + var tabs_box_owned = false; │ │46 + errdefer if (!tabs_box_owned) tabs_box.deinit(allocator); │ │47 + │ │48 var tab_ids: std.AutoArrayHashMapUnmanaged(usize, void) = .empty; │ │49 errdefer tab_ids.deinit(allocator); │ │50 │ ╰─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────╯ ╭────────────────────────────────────────────────────────────────────────╮ │40 - try ui.widget.addBackButton(allocator, &box, session); │ │51 + // the leading space plus the title │ │52 + const first_group_width = 1 + try data.title.width(); │ │53 + │ │54 + try ui.widget.addBackButton(allocator, &title_box, session);│ │55 │ │56 { │ │57 var text = try wgt.Text.init(allocator, " "); │ ╰────────────────────────────────────────────────────────────────────────╯ ╭────────────────────────────────────────────────────────────────────────────╮ │58 errdefer text.deinit(allocator); │ │45 - try box.children.put(allocator, text.getFocus().id, .{ │ │59 + try title_box.children.put(allocator, text.getFocus().id, .{│ │60 .widget = .{ .text = text }, │ │61 .rect = null, │ │62 .min_size = .{ .width = 1, .height = null }, │ ╰────────────────────────────────────────────────────────────────────────────╯ ╭──────────────────────────────────────────────────────────────────────────────────╮ │67 { │ │68 var title_view = try ui.Title.View.init(allocator, &data.title); │ │69 errdefer title_view.deinit(allocator); │ │56 - // shrink the title when there is not enough space │ │57 - try box.children.put(allocator, title_view.getFocus().id, .{ │ │70 + try title_box.children.put(allocator, title_view.getFocus().id, .{│ │71 .widget = .{ .title = title_view }, │ │72 .rect = null, │ │73 .min_size = null, │ ╰──────────────────────────────────────────────────────────────────────────────────╯ ╭────────────────────────────────────╮ │61 - .flex = .shrink,│ │74 }); │ │75 } │ │76 │ ╰────────────────────────────────────╯ ╭──────╮ │next →│ ╰──────╯