Mercurial > web-gnusto

changeset 70:16a460235f57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
The line height of buffered windows is now dynamically determined.
author Atul Varma <varmaa@toolness.com>
date Sun, 18 May 2008 23:21:28 -0700
parents 23f9e15fa690
children 65a960c019bb
files gnusto.css web-zui.js
diffstat 2 files changed, 11 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/gnusto.css	Sat May 17 13:44:15 2008 -0700
+++ b/gnusto.css	Sun May 18 23:21:28 2008 -0700
@@ -11,7 +11,6 @@
     margin: 0 auto;
     font-family: monaco, courier, courier new, monospace;
     font-size: 10pt;
-    line-height: 12pt;
     top: 0px;
     left: 0px;
     position: fixed;
--- a/web-zui.js	Sat May 17 13:44:15 2008 -0700
+++ b/web-zui.js	Sun May 18 23:21:28 2008 -0700
@@ -270,6 +270,7 @@
           newDiv.className = "buffered-window";
           newDiv.innerHTML = html;
           newDiv.style.width = self._pixelWidth + "px";
+          newDiv.style.lineHeight = self._pixelLineHeight + "px";
           $("#buffered-windows").append(newDiv);
 
           // Pretend the window was just resized, which will position
@@ -311,21 +312,27 @@
       }
     },
 
-    _getFixedPitchRowWidth: function() {
+    _setFixedPitchSizes: function() {
       var row = document.createElement("div");
       row.className = "buffered-window";
       for (var i = 0; i < self._size[0]; i++)
         row.innerHTML += "O";
+
+      // We have to wrap the text in a span to get an accurate line
+      // height value, for some reason...
+      row.innerHTML = "<span>" + row.innerHTML + "</span>";
+
       $("#buffered-windows").append(row);
-      var width = row.clientWidth;
+      self._pixelWidth = row.clientWidth;
+      self._pixelLineHeight = row.firstChild.offsetHeight;
       $("#buffered-windows").empty();
-      return width;
     }
   };
 
-  self._pixelWidth = self._getFixedPitchRowWidth();
+  self._setFixedPitchSizes();
 
   $("#top-window").get(0).style.width = self._pixelWidth + "px";
+  $("#top-window").get(0).style.lineHeight = self._pixelLineHeight + "px";
   $("#content").get(0).style.width = self._pixelWidth + "px";
 
   self._windowResize();