From 61f57ed631bed015b1453e9ffa3cd22e4f7bb254 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Thu, 16 Jun 2016 08:58:49 -0400
Subject: [PATCH] Fix stretch data for U+222B (integral) in STIX-Web data for
 HTML-CSS and SVG, and add it so local STIX data.  Resolves issue #1092.

---
 .../jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js  | 4 ++--
 unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js   | 2 +-
 unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js | 8 +++++++-
 unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js       | 1 +
 unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js  | 4 ++--
 unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js        | 2 +-
 6 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js
index 210b014d4..e7f77b4f4 100644
--- a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js
+++ b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js
@@ -415,9 +415,9 @@
       },
       0x222B:
       {
-        dir: H,
+        dir: V,
         HW: [[0.607,MAIN], [0.979,SIZE1]],
-        stretch: {top:[0xE03C,SIZE5], rep:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]}
+        stretch: {top:[0xE03C,SIZE5], ext:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]}
       },
       0x222C:
       {
diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js
index 461cd2f44..2909f8cb4 100644
--- a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js
+++ b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js
@@ -531,7 +531,7 @@
           HW: [[0.879,MAIN]],
           stretch: {ext:[0x2225,MAIN]}
         },
-        0x222B: EXTRAH,
+        0x222B: EXTRAV,
         0x222C: EXTRAV,
         0x222D: EXTRAV,
         0x222E: EXTRAV,
diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js
index ed0a16bd4..3c101e9b7 100644
--- a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js
+++ b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js
@@ -37,7 +37,8 @@
       SIZE2   = "STIXSizeTwoSym",
       SIZE3   = "STIXSizeThreeSym",
       SIZE4   = "STIXSizeFourSym",
-      SIZE5   = "STIXSizeFiveSym";
+      SIZE5   = "STIXSizeFiveSym",
+      INTD    = "STIXIntegralsD";
   var H = "H", V = "V";
   
   var delim = {
@@ -121,6 +122,11 @@
     {
       dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x21DB,GENERAL], rep:[0x2261,GENERAL]}
     },
+    0x222B: // integral
+    {
+      dir: V, HW: [[0.607,GENERAL], [0.979,INTD]],
+      stretch: {top:[0x2320,SIZE1], ext:[0x23AE,SIZE1], bot:[0x2321,SIZE1]}
+    },
     0x23B4: // top square bracket
     {
       dir: H, HW: [[.926,GENERAL],[1.063,SIZE1],[1.606,SIZE2],[2.147,SIZE3],[2.692,SIZE4],[3.237,SIZE5]],
diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js
index 920de949a..5643f987e 100644
--- a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js
+++ b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js
@@ -406,6 +406,7 @@
         0x21C3: EXTRAV, // down harpoon with barb left
         0x21DA: EXTRAH, // left triple arrow
         0x21DB: EXTRAH, // right triple arrow
+        0x222B: EXTRAV, // integral
         0x23B4: EXTRAH, // top square bracket
         0x23B5: EXTRAH, // bottom square bracket
         0x23DC: EXTRAH, // top paren
diff --git a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js
index 75280f595..44bb64fd7 100644
--- a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js
+++ b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js
@@ -415,9 +415,9 @@
       },
       0x222B:
       {
-        dir: H,
+        dir: V,
         HW: [[607,MAIN], [979,SIZE1]],
-        stretch: {top:[0xE03C,SIZE5], rep:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]}
+        stretch: {top:[0xE03C,SIZE5], ext:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]}
       },
       0x222C:
       {
diff --git a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js
index a2a26eb45..05c62ba6e 100644
--- a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js
+++ b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js
@@ -528,7 +528,7 @@
           HW: [[879,MAIN]],
           stretch: {ext:[0x2225,MAIN]}
         },
-        0x222B: EXTRAH,
+        0x222B: EXTRAV,
         0x222C: EXTRAV,
         0x222D: EXTRAV,
         0x222E: EXTRAV,