Varedit remembers search + minor styles (#10393)

Varedit now remembers what was in the 'search' field when you click the 'refresh' link. This makes our miserable lives a little less miserable.
    Tweaked varedit styles ever so slightly: it will now likely use a "better" monospace font depending on what's on your system. Var names are now bold and also monospace.
    The window spawns a tiny bit bigger.

code/js/view_variables.js

@@ -14,7 +14,10 @@ function updateSearch() {
 		} else {
 			li.style.display = "none";
 		}
-	}
+  }
+
+  var refresh_link = document.getElementById('refresh');
+  refresh_link.href = refresh_link.getAttribute('data-initial-href') + filter;
 }
 
 function selectTextField() {