exec keys: push_jump if editor has changed

This commit is contained in:
Maxime Coste 2013-02-07 13:35:21 +01:00
parent 785abfbad5
commit 6c7d646d35

View File

@ -534,7 +534,13 @@ void exec_keys(const KeyList& keys, Context& context)
batch_input_handler.context().change_editor(context.editor()); batch_input_handler.context().change_editor(context.editor());
batch_input_handler.handle_available_inputs(); batch_input_handler.handle_available_inputs();
context.change_editor(batch_input_handler.context().editor());
auto& new_editor = batch_input_handler.context().editor();
if (&new_editor != &context.editor())
{
context.push_jump();
context.change_editor(new_editor);
}
} }
template<typename Func> template<typename Func>