Fix a few things after #7166 (#7212)

* Switching between HTML/text dicts (Fix #7209)
* Updating the scrollbar and scroll state properly when switching dicts
* Highlights in SortWidget
* Highlights in the Dictionary Download page
* Minor simplification of the tail end of the update process in ImageViewer
This commit is contained in:
NiLuJe
2021-01-31 02:51:40 +01:00
committed by GitHub
parent 3118d0dba0
commit a38881a9f7
6 changed files with 163 additions and 141 deletions

View File

@@ -50,7 +50,7 @@ function ScrollHtmlWidget:init()
end
}
self.v_scroll_bar:set((self.htmlbox_widget.page_number-1) / self.htmlbox_widget.page_count, self.htmlbox_widget.page_number / self.htmlbox_widget.page_count)
self:_updateScrollBar()
local horizontal_group = HorizontalGroup:new{}
table.insert(horizontal_group, self.htmlbox_widget)
@@ -85,10 +85,25 @@ function ScrollHtmlWidget:init()
end
end
-- Not to be confused with ScrollTextWidget's updateScrollBar, which has user-visible effects.
-- This simply updates the scroll bar's internal state according to the current page & page count.
function ScrollHtmlWidget:_updateScrollBar()
self.v_scroll_bar:set((self.htmlbox_widget.page_number-1) / self.htmlbox_widget.page_count, self.htmlbox_widget.page_number / self.htmlbox_widget.page_count)
end
function ScrollHtmlWidget:getSinglePageHeight()
return self.htmlbox_widget:getSinglePageHeight()
end
-- Reset the scrolling *state* to the top of the document, but don't actually re-render/refresh anything.
-- (Useful when replacing a Scroll*Widget during an update call, c.f., DictQuickLookup).
function ScrollHtmlWidget:resetScroll()
self.htmlbox_widget.page_number = 1
self:_updateScrollBar()
self.v_scroll_bar.enable = self.htmlbox_widget.page_count > 1
end
function ScrollHtmlWidget:scrollToRatio(ratio)
ratio = math.max(0, math.min(1, ratio)) -- ensure ratio is between 0 and 1 (100%)
local page_num = 1 + math.floor((self.htmlbox_widget.page_count) * ratio)
@@ -99,9 +114,11 @@ function ScrollHtmlWidget:scrollToRatio(ratio)
return
end
self.htmlbox_widget.page_number = page_num
self.v_scroll_bar:set((page_num-1) / self.htmlbox_widget.page_count, page_num / self.htmlbox_widget.page_count)
self:_updateScrollBar()
self.htmlbox_widget:freeBb()
self.htmlbox_widget:_render()
UIManager:setDirty(self.dialog, function()
return "partial", self.dimen
end)
@@ -125,8 +142,7 @@ function ScrollHtmlWidget:scrollText(direction)
self.htmlbox_widget.page_number = self.htmlbox_widget.page_number - 1
end
self.v_scroll_bar:set((self.htmlbox_widget.page_number-1) / self.htmlbox_widget.page_count, self.htmlbox_widget.page_number / self.htmlbox_widget.page_count)
self:_updateScrollBar()
self.htmlbox_widget:freeBb()
self.htmlbox_widget:_render()