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
}
+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)
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);
}