]> git.lyx.org Git - lyx.git/blobdiff - src/Session.cpp
Avoid full metrics computation with Update:FitCursor
[lyx.git] / src / Session.cpp
index f8d611644ca94a523dff11eadd26d418cea77114..9ec18f1d0141852646217929a47bd1563abb2f62 100644 (file)
@@ -31,11 +31,12 @@ string const sec_lastfiles = "[recent files]";
 string const sec_lastfilepos = "[cursor positions]";
 string const sec_lastopened = "[last opened files]";
 string const sec_bookmarks = "[bookmarks]";
-string const sec_session = "[session info]";
-string const sec_toolbars = "[toolbars]";
 string const sec_lastcommands = "[last commands]";
 string const sec_authfiles = "[auth files]";
 string const sec_shellescape = "[shell escape files]";
+// currently unused:
+//string const sec_session = "[session info]";
+//string const sec_toolbars = "[toolbars]";
 
 } // namespace
 
@@ -339,6 +340,29 @@ BookmarksSection::Bookmark const & BookmarksSection::bookmark(unsigned int i) co
 }
 
 
+BookmarksSection::BookmarkPosList
+BookmarksSection::bookmarksInPar(FileName const & fn, int const par_id) const
+{
+       // FIXME: we do not consider the case of bottom_pit.
+       // This is probably not a problem.
+       BookmarksSection::BookmarkPosList bip;
+       for (size_t i = 1; i < bookmarks.size(); ++i)
+               if (bookmarks[i].filename == fn && bookmarks[i].top_id == par_id)
+                       bip.push_back({i, bookmarks[i].top_pos});
+
+       return bip;
+}
+
+
+void BookmarksSection::adjustPosAfterPos(FileName const & fn,
+       int const par_id, pos_type pos, int offset)
+{
+       for (Bookmark & bkm : bookmarks)
+               if (bkm.filename == fn && bkm.top_id == par_id && bkm.top_pos > pos)
+                       bkm.top_pos += offset;
+}
+
+
 LastCommandsSection::LastCommandsSection(unsigned int num) :
        default_num_last_commands(30),
        absolute_max_last_commands(100)
@@ -385,6 +409,11 @@ void LastCommandsSection::setNumberOfLastCommands(unsigned int no)
 
 void LastCommandsSection::add(std::string const & command)
 {
+       // remove traces of 'command' in history using the erase-remove idiom
+       //   https://en.wikipedia.org/wiki/Erase%E2%80%93remove_idiom
+       lastcommands.erase(remove(lastcommands.begin(), lastcommands.end(), command),
+                          lastcommands.end());
+       // add it at the end of the list.
        lastcommands.push_back(command);
 }