www

commit 36194fe36aa3f6f2d875fef0c163926486017fe4
parent 4ea4816553cf794894b6aec9a710242a7ec19128
Author: Davide P. Cervone <dpvc@union.edu>
Date:   Sat, 22 Feb 2014 14:31:37 -0500

Add a new fonts parameter for HTML-CSS to simplify font configuration.

Diffstat:
M
unpacked/jax/output/HTML-CSS/jax.js
 | 
7
++++++-

1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/unpacked/jax/output/HTML-CSS/jax.js b/unpacked/jax/output/HTML-CSS/jax.js
@@ -370,7 +370,7 @@
       if (this.adjustAvailableFonts) {this.adjustAvailableFonts(config.availableFonts)}
       if (settings.scale) {config.scale = settings.scale}
       if (font && font !== "Auto" && this.fontName[font]) {
-        config.availableFonts = [];
+        config.availableFonts = []; delete config.fonts;
         if (this.fontName[font] instanceof Array) {
           config.preferredFont = this.fontName[font][0];
           config.webFont = this.fontName[font][1];
@@ -379,6 +379,11 @@
         }
         if (config.preferredFont) {config.availableFonts[0] = config.preferredFont}
       }
+      if (config.fonts) {
+        config.availableFonts = config.fonts;
+        config.preferredFont = config.webFont = config.fonts[0];
+        if (config.webFont === "STIX") {config.webFont += "-Web"}
+      }
       font = this.Font.findFont(config.availableFonts,config.preferredFont);
       if (!font && this.allowWebFonts) {font = config.webFont; if (font) {this.webFonts = true}}
       if (!font && this.config.imageFont) {font = config.imageFont; this.imgFonts = true}