Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

diff: minor cleanup of unchanged regions #4629

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

diff: minor cleanup of unchanged regions #4629

wants to merge 4 commits into from

Commits on Oct 12, 2024

  1. diff: simplify merge of refined ranges, unimplement Ord 

    The Ord implementation didn't conform to Eq (which compares "self.others"
literally), and we don't need Ord to insert non-overlapping ranges before the
current range.
    @yuja
    yuja committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    5cdc126 View commit details
    Browse the repository at this point in the history

  2. diff: omit insertion of terminal range that would be compacted 

    This isn't important, but I'm going to add another empty range at the start,
and it's easier if the modification of regions is scoped.
    @yuja
    yuja committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    a2e20e5 View commit details
    Browse the repository at this point in the history

  3. diff: insert empty unchanged range at start to remove some clone()s 

    This seems more consistent as we have a terminal range at the end.
    @yuja
    yuja committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    bf2c1bb View commit details
    Browse the repository at this point in the history

  4. diff: rely on compacted unchanged regions when iterating hunks 

    We don't have to test emptiness of contents between unchanged regions.
    @yuja
    yuja committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    6f30d0b View commit details
    Browse the repository at this point in the history