From 19a0ef3afe182d91afb435015cda6e1bef1fabc3 Mon Sep 17 00:00:00 2001
From: Thierry Parmentelat <thierry.parmentelat@inria.fr>
Date: Wed, 20 Mar 2013 10:49:09 +0100
Subject: [PATCH] cosmetic changes to the plugin layout

---
 unfold/css/plugin.css        | 13 +++++++++----
 unfold/templates/plugin.html |  8 ++++----
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/unfold/css/plugin.css b/unfold/css/plugin.css
index d2da242a..910ff4fd 100644
--- a/unfold/css/plugin.css
+++ b/unfold/css/plugin.css
@@ -1,21 +1,26 @@
 div.plugin-toggle {
-    padding:		4px;
+    margin:		3px;
+    padding:		5px;
     border-style:	dotted;
     border-width:	1px;
     border-radius:	8px;
 }
-p.plugin-show {
+h4.plugin-show {
     cursor: s-resize;
 }
-p.plugin-hide { 
+h4.plugin-hide { 
     cursor: n-resize;
 }
+h4.plugin-show, h4.plugin-hide {
+    margin:8px;
+}
 i.icon-hand-right,i.icon-hand-down {
     padding-right: 4px;
 }
 a.plugin-tooltip { 
-    font-size: 150%;
+    font-size: 130%;
     font-style: italic;
+    font-weight: normal;
     padding: 4px;
     color: #808080;
 }
diff --git a/unfold/templates/plugin.html b/unfold/templates/plugin.html
index 1979eb95..c77ad6f0 100644
--- a/unfold/templates/plugin.html
+++ b/unfold/templates/plugin.html
@@ -2,10 +2,10 @@
 {% if visible %}
 <div class='plugin-toggle{% if need_spin %} need-spin{% endif %}' id='toggle-{{ domid }}'>
 {% if togglable %}
-<span id='show-{{ domid }}' class='plugin-show'{% if toggled %} style='display:none;'{% endif %}><i class="icon-hand-right"></i>
-<a href='#' class='plugin-tooltip' data-toggle='tooltip' data-original-title='Show plugin "{{ title }}" ({{ classname }})'>{{ title }}</a></span>
-<span id='hide-{{ domid }}' class='plugin-hide'{% if not toggled %} style='display:none;'{% endif %}><i class="icon-hand-down"></i>
-<a href='#' class='plugin-tooltip' data-toggle='tooltip' data-original-title='Hide plugin "{{ title }}" ({{ classname }})'>{{ title }}</a></span>
+<h4 id='show-{{ domid }}' class='plugin-show'{% if toggled %} style='display:none;'{% endif %}><i class="icon-hand-right"></i>
+<a href='#' class='plugin-tooltip' data-toggle='tooltip' data-original-title='Show plugin "{{ title }}" ({{ classname }})'>{{ title }}</a></h4>
+<h4 id='hide-{{ domid }}' class='plugin-hide'{% if not toggled %} style='display:none;'{% endif %}><i class="icon-hand-down"></i>
+<a href='#' class='plugin-tooltip' data-toggle='tooltip' data-original-title='Hide plugin "{{ title }}" ({{ classname }})'>{{ title }}</a></h4>
 {% endif %}{# togglable #}
 {% endif %}{# visible #}
 
-- 
2.43.0