if ($highlight-theme == 'normal') {
  $highlight-deletion = #fdd;
  $highlight-addition = #dfd;
} else {
  $highlight-deletion = #800000;
  $highlight-addition = #008000;
}