Updated switch_panel documentation

src/gui/widgets/panel-bar.hpp

@@ -75,6 +75,8 @@ private:
 
   /**
    * An event handler for when a panel type is chosen.
+   * @param type_index The index of the panel description that will be
+   * instantiated.
    **/
   void on_panel_type(int type_index);
 

src/gui/workspace/panel-manager.hpp

@@ -81,6 +81,13 @@ public:
    **/
   WorkspaceWindow& get_workspace_window();
   
+  /**
+   * Switches a panel from one type to another, without touching the
+   * underlying GdlDockItem.
+   * @param old_panel The panel which will be transofrmed to a new type.
+   * @param new_panel_description_index The index of the panel
+   * description that will be instantiated.
+   **/
   void switch_panel(panels::Panel &old_panel,
     int new_panel_description_index);