From b2504562731462676f8c6bce561a115742bf470b Mon Sep 17 00:00:00 2001
From: Benjamin Jones <bjones@galois.com>
Date: Thu, 25 Oct 2012 17:37:33 -0700
Subject: changed API of fiveui.font.validate so the allow object has arrays as
 leaves

---
 contexts/data/fiveui/injected/prelude.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contexts/data/fiveui/injected/prelude.js b/contexts/data/fiveui/injected/prelude.js
index 576ccc8..eb9b0dd 100644
--- a/contexts/data/fiveui/injected/prelude.js
+++ b/contexts/data/fiveui/injected/prelude.js
@@ -308,7 +308,7 @@ fiveui.font.getFont = function (jElt) {
  * <p><pre>
  * EXAMPLES::
  *
- *   > allow = { 'Verdana': { 'bold': {"10":{}, "12":{}}, 'normal': {"10":{}, "12":{}} } };
+ *   > allow = { 'Verdana': { 'bold': [10, 12], 'normal': [10, 12]}};
  *   > font = { family: 'Verdana Arial sans-serif', size: "10", weight: "normal" };
  *   > fiveui.font.validate(allow, font) -> true
  * </pre></p>
@@ -323,7 +323,7 @@ fiveui.font.validate = function (allow, font) {
     if (font.family.indexOf(x) != -1) { break; }
     else { return false; }
   }
-  return (font.weight in allow[x] && font.size in allow[x][font.weight]);
+  return (font.weight in allow[x] &&  allow[x][font.weight].indexOf(parseInt(font.size)) != -1);
 };
 
 /**
-- 
cgit v1.2.3