function resize_nav_table(){
  var new_size = document.getElementById("main").scrollHeight;
  new_size = new_size < 550?550:new_size;
  var nav = document.getElementById("nav");
  var rule = document.getElementById("vert_rule");
  nav.style.height = new_size + "px";
  rule.style.height = new_size + "px";
  
}