[latexila] File browser: remove refresh button

[SÃbastien Wilmet <swilmet src gnome org>]

commit 2f6e688636de5eda428e24d0bb3efa0af207bc32
Author: SÃbastien Wilmet <swilmet gnome org>
Date:   Wed Aug 8 01:16:58 2012 +0200

    File browser: remove refresh button
    
    It will be replaced by a directory monitor, to automatically refresh the
    directory.

 src/file_browser.vala            |  153 ++++++++++++++++----------------------
 src/main_window.vala             |    1 -
 src/main_window_build_tools.vala |   22 +-----
 3 files changed, 66 insertions(+), 110 deletions(-)
---
diff --git a/src/file_browser.vala b/src/file_browser.vala
index c1b2e92..688fa05 100644
--- a/src/file_browser.vala
+++ b/src/file_browser.vala
@@ -67,6 +67,9 @@ public class FileBrowser : Grid
         set_directory (get_default_directory ());
     }
 
+    /*************************************************************************/
+    // Init functions
+
     private void init_settings ()
     {
         _settings = new GLib.Settings ("org.gnome.latexila.preferences.file-browser");
@@ -79,21 +82,6 @@ public class FileBrowser : Grid
         _latex_settings.changed["clean-extensions"].connect (delayed_refresh);
     }
 
-    private void delayed_refresh ()
-    {
-        // Call refresh () only after 2 seconds.
-        // If the text has changed before the 2 seconds, we reinitialize the counter.
-        if (_timeout_id != 0)
-            Source.remove (_timeout_id);
-
-        _timeout_id = Timeout.add_seconds (2, () =>
-        {
-            _timeout_id = 0;
-            refresh ();
-            return false;
-        });
-    }
-
     private void init_toolbar ()
     {
         Grid grid = new Grid ();
@@ -104,17 +92,14 @@ public class FileBrowser : Grid
         Button home_button = Utils.get_toolbar_button (Stock.HOME);
         _parent_button = Utils.get_toolbar_button (Stock.GO_UP);
         Button jump_button = Utils.get_toolbar_button (Stock.JUMP_TO);
-        Button refresh_button = Utils.get_toolbar_button (Stock.REFRESH);
 
         home_button.tooltip_text = _("Go to the home directory");
         _parent_button.tooltip_text = _("Go to the parent directory");
         jump_button.tooltip_text = _("Go to the active document directory");
-        refresh_button.tooltip_text = _("Refresh");
 
         grid.add (home_button);
         grid.add (_parent_button);
         grid.add (jump_button);
-        grid.add (refresh_button);
 
         home_button.clicked.connect (() =>
         {
@@ -151,14 +136,6 @@ public class FileBrowser : Grid
                 });
             }
         });
-
-        refresh_button.clicked.connect (refresh);
-    }
-
-    private void update_jump_button_sensitivity (Button jump_button)
-    {
-        jump_button.sensitive = _main_window.active_tab != null
-            && _main_window.active_document.location != null;
     }
 
     // list of parent directories
@@ -276,69 +253,8 @@ public class FileBrowser : Grid
         });
     }
 
-    private void refresh ()
-    {
-        set_directory (_current_directory, true);
-    }
-
-    // Refresh the file browser if the document has a "link" with the directory currently
-    // displayed.
-    public void refresh_for_document (Document doc)
-    {
-        Project? project = doc.get_project ();
-
-        // If the document is not part of a project, refresh only if the document's
-        // directory is the same as the current directory.
-        if (project == null)
-        {
-            if (doc.location != null
-                && _current_directory.equal (doc.location.get_parent ()))
-            {
-                refresh ();
-            }
-
-            return;
-        }
-
-        // If a project is defined, refresh if the current dir is part of the project.
-        File project_dir = project.directory;
-
-        if (_current_directory.equal (project_dir)
-            || _current_directory.has_prefix (project_dir))
-        {
-            refresh ();
-        }
-    }
-
-    // Get the previous directory saved in GSettings, or the user home directory as
-    // a fallback.
-    private File get_default_directory ()
-    {
-        string? uri = _settings.get_string ("current-directory");
-
-        if (uri != null && uri != "")
-        {
-            File directory = File.new_for_uri (uri);
-
-            if (directory.query_exists ())
-                return directory;
-        }
-
-        return File.new_for_path (Environment.get_home_dir ());
-    }
-
-    private void set_directory (File directory, bool force = false)
-    {
-        if (! force && _current_directory == directory)
-            return;
-
-        _current_directory = directory;
-        _settings.set_string ("current-directory", directory.get_uri ());
-        _parent_button.set_sensitive (directory.get_parent () != null);
-
-        update_parent_directories ();
-        update_list ();
-    }
+    /*************************************************************************/
+    // Update the list of parent directories and the list of files
 
     private void update_parent_directories ()
     {
@@ -492,6 +408,65 @@ public class FileBrowser : Grid
         );
     }
 
+    /*************************************************************************/
+    // Misc
+
+    private void refresh ()
+    {
+        set_directory (_current_directory, true);
+    }
+
+    private void delayed_refresh ()
+    {
+        // Call refresh () only after 2 seconds.
+        // If the text has changed before the 2 seconds, we reinitialize the counter.
+        if (_timeout_id != 0)
+            Source.remove (_timeout_id);
+
+        _timeout_id = Timeout.add_seconds (2, () =>
+        {
+            _timeout_id = 0;
+            refresh ();
+            return false;
+        });
+    }
+
+    // Get the previous directory saved in GSettings, or the user home directory as
+    // a fallback.
+    private File get_default_directory ()
+    {
+        string? uri = _settings.get_string ("current-directory");
+
+        if (uri != null && uri != "")
+        {
+            File directory = File.new_for_uri (uri);
+
+            if (directory.query_exists ())
+                return directory;
+        }
+
+        return File.new_for_path (Environment.get_home_dir ());
+    }
+
+    private void set_directory (File directory, bool force = false)
+    {
+        if (! force && _current_directory == directory)
+            return;
+
+        _current_directory = directory;
+        _settings.set_string ("current-directory", directory.get_uri ());
+        _parent_button.set_sensitive (directory.get_parent () != null);
+
+        update_parent_directories ();
+        update_list ();
+    }
+
+    private void update_jump_button_sensitivity (Button jump_button)
+    {
+        jump_button.sensitive = _main_window.active_tab != null
+            && _main_window.active_document.location != null;
+    }
+
     private int on_sort (TreeModel model, TreeIter a, TreeIter b)
     {
         bool a_is_dir, b_is_dir;
diff --git a/src/main_window.vala b/src/main_window.vala
index fb5c43d..4dcda5b 100644
--- a/src/main_window.vala
+++ b/src/main_window.vala
@@ -374,7 +374,6 @@ public class MainWindow : Window
 
         // File browser
         FileBrowser file_browser = new FileBrowser (this);
-        _main_window_build_tools.set_file_browser (file_browser);
         side_panel.add_component (_("File Browser"), Stock.OPEN, file_browser);
 
         // Structure
diff --git a/src/main_window_build_tools.vala b/src/main_window_build_tools.vala
index baa4138..301c83e 100644
--- a/src/main_window_build_tools.vala
+++ b/src/main_window_build_tools.vala
@@ -56,7 +56,6 @@ public class MainWindowBuildTools
     private unowned MainWindow _main_window;
     private UIManager _ui_manager;
     private BuildView _build_view;
-    private FileBrowser _file_browser;
     private BottomPanel _bottom_panel;
 
     private Gtk.ActionGroup _static_action_group;
@@ -98,12 +97,6 @@ public class MainWindowBuildTools
         connect_toggle_actions ();
     }
 
-    public void set_file_browser (FileBrowser file_browser)
-    {
-        // TODO It would be better if the file browser could detect files updates.
-        _file_browser = file_browser;
-    }
-
     public void set_bottom_panel (BottomPanel bottom_panel)
     {
         _bottom_panel = bottom_panel;
@@ -306,7 +299,6 @@ public class MainWindowBuildTools
     {
         return_if_fail (_main_window.active_tab != null);
         return_if_fail (_build_view != null);
-        return_if_fail (_file_browser != null);
         return_if_fail (_bottom_panel != null);
 
         BuildTool? tool = get_build_tool_from_name (action.name);
@@ -353,15 +345,7 @@ public class MainWindowBuildTools
 
         File main_file = active_doc.get_main_file ();
         _build_tool_runner = new BuildToolRunner (tool, main_file, _build_view);
-
-        _build_tool_runner.finished.connect (() =>
-        {
-            stop_exec.sensitive = false;
-
-            if (tool.has_jobs ())
-                _file_browser.refresh_for_document (active_doc);
-        });
-
+        _build_tool_runner.finished.connect (() => stop_exec.sensitive = false);
         _build_tool_runner.run ();
     }
 
@@ -416,13 +400,11 @@ public class MainWindowBuildTools
     public void on_clean ()
     {
         return_if_fail (_main_window.active_tab != null);
-        return_if_fail (_file_browser != null);
 
         CleanBuildFiles build_files = new CleanBuildFiles (_main_window,
             _main_window.active_document);
 
-        if (build_files.clean ())
-            _file_browser.refresh_for_document (_main_window.active_document);
+        build_files.clean ();
     }
 
     public void on_view_log ()