Fixed bug in textinput::adjust_vertical concerning selection_origin update

This bug was discovered using the F* formal verification framework.

Style changes (match -> if let)

Replace if let Some(_) by .is_some()
This commit is contained in:
Denis Merigoux 2018-12-14 14:21:50 +01:00
parent 9ca6768a56
commit e1ea8fbd35
2 changed files with 26 additions and 1 deletions

View file

@ -442,12 +442,23 @@ impl<T: ClipboardProvider> TextInput<T> {
let target_line: isize = self.edit_point.line as isize + adjust;
if target_line < 0 {
self.edit_point.index = 0;
self.edit_point.line = 0;
self.edit_point.index = 0;
if self.selection_origin.is_some() &&
(self.selection_direction == SelectionDirection::None ||
self.selection_direction == SelectionDirection::Forward)
{
self.selection_origin = Some(TextPoint { line: 0, index: 0 });
}
return;
} else if target_line as usize >= self.lines.len() {
self.edit_point.line = self.lines.len() - 1;
self.edit_point.index = self.current_line_length();
if self.selection_origin.is_some() &&
(self.selection_direction == SelectionDirection::Backward)
{
self.selection_origin = Some(self.edit_point);
}
return;
}
@ -456,6 +467,16 @@ impl<T: ClipboardProvider> TextInput<T> {
.count();
self.edit_point.line = target_line as usize;
self.edit_point.index = len_of_first_n_chars(&self.lines[self.edit_point.line], col);
if let Some(origin) = self.selection_origin {
if ((self.selection_direction == SelectionDirection::None ||
self.selection_direction == SelectionDirection::Forward) &&
self.edit_point <= origin) ||
(self.selection_direction == SelectionDirection::Backward &&
origin <= self.edit_point)
{
self.selection_origin = Some(self.edit_point);
}
}
self.assert_ok_selection();
}

View file

@ -318,6 +318,10 @@ fn test_textinput_adjust_vertical() {
textinput.adjust_vertical(2, Selection::NotSelected);
assert_eq!(textinput.edit_point().line, 2);
assert_eq!(textinput.edit_point().index, 1);
textinput.adjust_vertical(-1, Selection::Selected);
assert_eq!(textinput.edit_point().line, 1);
assert_eq!(textinput.edit_point().index, 1);
}
#[test]