Bookmarks: new settings and tweaks (#8301)

Bookmarks list:
- page numbers are displayed
- page bookmarks are marked with a star
- new setting: Sort by largest page number (default: checked)
New bookmark setting: Add page number / timestamp to bookmark
- If enabled (default), bookmark name is 'Page # notes @ time'.
- If disabled, bookmark name is equal to the notes field.
Rename bookmark dialog:
- page number and timestamp are displayed in the input
  dialog description
- blank input renames bookmark to the default name in
  accordance with the new setting
Also fix: changing boundaries of the highlight: the name of the
highlight is not changed if it was previously edited by the user.
This commit is contained in:
hius07
2021-10-18 18:26:04 +03:00
committed by GitHub
parent fd697f3c77
commit f0b992d425
2 changed files with 185 additions and 122 deletions

View File

@@ -35,9 +35,7 @@ local order = {
"toc_items_font_size",
"toc_items_with_dots",
"----------------------------",
"bookmarks_items_per_page",
"bookmarks_items_font_size",
"bookmarks_items_show_more_text",
"bookmarks_settings",
},
typeset = {
"set_render_style",