# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1253046444 14400
# Node ID 2412cb10c97cf471109f903f4239225e40932cac
# Parent  7710f65935b66a53dd27f1e59e7d85ac534ec02b
Filters displaying properly

diff -r 7710f65935b6 -r 2412cb10c97c demo/more/dbgrid.ur
--- a/demo/more/dbgrid.ur	Tue Sep 15 16:06:12 2009 -0400
+++ b/demo/more/dbgrid.ur	Tue Sep 15 16:27:24 2009 -0400
@@ -109,7 +109,11 @@
                               Parse = fn s => v <- signal s; return (m.Parse v),
                               CreateFilter = source m.CreateFilter,
                               DisplayFilter = m.DisplayFilter,
-                              Filter = fn f v => f <- signal f; return (m.Filter f v)},
+                              Filter = fn f v => f <- signal f;
+                                          return (if m.FilterIsNull f then
+                                                      True
+                                                  else
+                                                      m.Filter f v)},
                              {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
                               Edit = m.Edit,
                               Initialize = fn v => source (case v of
@@ -126,7 +130,7 @@
                               DisplayFilter = m.DisplayFilter,
                               Filter = fn f v => f <- signal f;
                                           return (if m.FilterIsNull f then
-                                                      Option.isNone v
+                                                      True
                                                   else
                                                       case v of
                                                           None => False
@@ -143,13 +147,13 @@
     type intFilter = basicFilter string
     val int : meta (intGlobal, int, intInput, intFilter) =
         basic {Display = fn s => <xml>{[s]}</xml>,
-               Edit = fn s => <xml><ctextbox source={s}/></xml>,
+               Edit = fn s => <xml><ctextbox size={5} source={s}/></xml>,
                Initialize = fn n => show n,
                InitializeNull = "",
                IsNull = eq "",
                Parse = fn v => read v,
                CreateFilter = "",
-               DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
+               DisplayFilter = fn s => <xml><ctextbox size={5} source={s}/></xml> : xbody,
                Filter = fn s n =>
                            case read s of
                                None => True
diff -r 7710f65935b6 -r 2412cb10c97c lib/js/urweb.js
--- a/lib/js/urweb.js	Tue Sep 15 16:06:12 2009 -0400
+++ b/lib/js/urweb.js	Tue Sep 15 16:27:24 2009 -0400
@@ -304,20 +304,22 @@
       runScripts(dummy);
       var table = x.parentNode;
 
-      var arr = dummy.getElementsByTagName("tbody");
-      firstChild = null;
-      var tbody;
-      if (arr.length > 0 && table != null)
-        tbody = arr[0];
-      else
-        tbody = dummy;
+      if (table) {
+        var arr = dummy.getElementsByTagName("tbody");
+        firstChild = null;
+        var tbody;
+        if (arr.length > 0 && table != null)
+          tbody = arr[0];
+        else
+          tbody = dummy.firstChild;
 
-      var next;
-      firstChild = document.createElement("script");
-      table.insertBefore(firstChild, x);
-      for (var node = tbody.firstChild; node; node = next) {
-        next = node.nextSibling;
-        table.insertBefore(node, x);
+        var next;
+        firstChild = document.createElement("script");
+        table.insertBefore(firstChild, x);
+        for (var node = tbody.firstChild; node; node = next) {
+          next = node.nextSibling;
+          table.insertBefore(node, x);
+        }
       }
     } else if (pnode == "tr") {
       var dummy = document.createElement("body");
@@ -325,10 +327,16 @@
       runScripts(dummy);
       var table = x.parentNode;
 
-      var arr = dummy.getElementsByTagName("tr");
-      firstChild = null;
-      if (arr.length > 0 && table != null) {
-        var tbody = arr[0], next;
+      if (table) {
+        var arr = dummy.getElementsByTagName("tr");
+        firstChild = null;
+        var tbody;
+        if (arr.length > 0 && table != null)
+          tbody = arr[0];
+        else
+          tbody = dummy.firstChild;
+
+        var next;
         firstChild = document.createElement("script");
         table.insertBefore(firstChild, x);
         for (var node = tbody.firstChild; node; node = next) {