class WorkAreaManager
{
public:
+ ///
WorkAreaManager() {}
-
///
void add(WorkArea * wa);
-
///
void remove(WorkArea * wa);
-
///
- void redrawAll();
-
+ void redrawAll(bool update_metrics);
///
void closeAll();
+ /// Update window titles of all users.
+ void updateTitles();
private:
+ typedef std::list<WorkArea *>::iterator iterator;
+ ///
std::list<WorkArea *> work_areas_;
};