function changeFont(file_name){
      var path="http://206.205.251.11:8080/gridsphere/html/";      
      var css_link = path+file_name;
      var elt = document.getElementById("font"); 
      elt.href=css_link;
 }