fix(drawing): make update_this_and_outward_bows fail graceful (with temporary fix)

This commit is contained in:
Ellen Emilia Anna Zscheile 2025-03-29 16:08:39 +01:00 committed by mikolaj
parent a56628e250
commit f6a196aeca
1 changed files with 19 additions and 4 deletions

View File

@ -534,14 +534,11 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
} }
} }
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))] fn update_this_and_outward_bows_intern(
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn update_this_and_outward_bows(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
around: LooseBendIndex, around: LooseBendIndex,
) -> Result<(), DrawingException> { ) -> Result<(), DrawingException> {
// FIXME: Fail gracefully on infringement.
let mut maybe_rail = Some(around); let mut maybe_rail = Some(around);
while let Some(rail) = maybe_rail { while let Some(rail) = maybe_rail {
@ -594,6 +591,24 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(()) Ok(())
} }
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn update_this_and_outward_bows(
&mut self,
recorder: &mut DrawingEdit<CW>,
around: LooseBendIndex,
) -> Result<(), DrawingException> {
let mut temp_recorder = DrawingEdit::new();
let ret = self.update_this_and_outward_bows_intern(&mut temp_recorder, around);
if ret.is_ok() {
recorder.apply(&temp_recorder);
} else {
temp_recorder.reverse_inplace();
self.recording_geometry_with_rtree.apply(&temp_recorder);
}
ret
}
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 4))] #[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 4))]
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() >= old(self.recording_geometry_with_rtree.graph().edge_count() + 5))] #[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() >= old(self.recording_geometry_with_rtree.graph().edge_count() + 5))]
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]