I just wanted to point out a redundant call to fetching a post from the db. In post.php line 51:
$post = get_post($post_ID);
Then later we do this:
$post = get_post_to_edit($post_ID);
The get_post_to_edit function also calls get_post, so it's doing the same thing twice. While not a huge issue (i mean how many users could be editing a post at once?), it would be better coding to not perform redundant trips to the db.