#52 closeFile bug

[Jacques-Henri Jourdan]

If the user closes a file which is not the current file, when the closeFile callback returns false, the contents of the file for which the user has clicked on the close file button becames the content of the (old) current file.

The fix I have found is to modify these lines in the edit_area_functions.js file :

EditArea.prototype.close_file= function(id){
if(this.files[id])
{
this.save_file(id);

// close file callback
if(this.execCommand('file_close', this.files[id])!==false)
{

by adding the command this.switch_to_file(id); :

if(this.files[id])
{
this.switch_to_file(id);
this.save_file(id);

// close file callback
if(this.execCommand('file_close', this.files[id])!==false)
{