mediawiki-extensions-Math/modules/MathJax/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js

/* -*- Mode: Javascript; indent-tabs-mode:nil; js-indent-level: 2 -*- */
/* vim: set ts=2 et sw=2 tw=80: */

/*************************************************************
 *
 *  MathJax/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js
 *  
 *  Adds extra stretchy characters to the STIX data.
 *
 *  ---------------------------------------------------------------------
 *  
 *  Copyright (c) 2011-2013 The MathJax Consortium
 *
 *  Licensed under the Apache License, Version 2.0 (the "License");
 *  you may not use this file except in compliance with the License.
 *  You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 *  Unless required by applicable law or agreed to in writing, software
 *  distributed under the License is distributed on an "AS IS" BASIS,
 *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 *  See the License for the specific language governing permissions and
 *  limitations under the License.
 */

(function (HTMLCSS) {
  var VERSION = "2.3";
  
  var DELIMITERS = HTMLCSS.FONTDATA.DELIMITERS;

  var GENERAL = "STIXGeneral",
      BOLD    = "STIXGeneral-bold",
      VARIANT = "STIXVariants",
      NONUNI  = "STIXNonUnicode",
      SIZE1   = "STIXSizeOneSym",
      SIZE2   = "STIXSizeTwoSym",
      SIZE3   = "STIXSizeThreeSym",
      SIZE4   = "STIXSizeFourSym",
      SIZE5   = "STIXSizeFiveSym";
  var H = "H", V = "V";
  
  var delim = {
    0x003D: // equal sign
    {
      dir: H, HW: [[.685,GENERAL]], stretch: {rep:[0x003D,GENERAL]}
    },
    0x219E: // left two-headed arrow
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {left:[0x219E,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21A0: // right two-headed arrow
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x21A0,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21A4: // left arrow from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x2190,VARIANT], rep:[0x2212,GENERAL], right:[0x22A3,BOLD,0,.1,.6]}
    },
    0x21A5: // up arrow from bar
    {
      dir: V, HW: [[.816,GENERAL]],
      stretch: {bot:[0x5F,GENERAL,.05,-.01,.8], ext:[0x23D0,GENERAL], top:[0x2191,GENERAL]}
    },
    0x21A6: // right arrow from bar
    {
      dir: H, HW: [[1,GENERAL]],
      stretch: {left:[0xE0B6,NONUNI], rep:[0x2212,GENERAL], right:[0x2192,GENERAL]}
    },
    0x21A7: // down arrow from bar
    {
      dir: V, HW: [[.816,GENERAL]],
      stretch: {top:[0x22A4,BOLD,0.04,0,.6], ext:[0x23D0,GENERAL], bot:[0x2193,GENERAL]}
    },
    0x21B0: // up arrow with top leftwards
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x21B0,GENERAL], ext:[0x23D0,GENERAL,.152]}
    },
    0x21B1: // up arrow with top right
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x21B1,GENERAL], ext:[0x23D0,GENERAL,-.195]}
    },
    0x21BC: // left harpoon with barb up
    {
      dir: H, HW: [[.955,GENERAL]], stretch: {left:[0x21BC,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21BD: // left harpoon with barb down
    {
      dir: H, HW: [[.955,GENERAL]], stretch: {left:[0x21BD,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21BE: // up harpoon with barb right
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x21BE,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x21BF: // up harpoon with barb left
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x21BF,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x21C0: // right harpoon with barb up
    {
      dir: H, HW: [[.955,GENERAL]], stretch: {right:[0x21C0,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21C1: // right harpoon with barb down
    {
      dir: H, HW: [[.955,GENERAL]], stretch: {right:[0x21C1,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21C2: // down harpoon with barb right
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x21C2,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x21C3: // down harpoon with barb left
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x21C3,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x21DA: // left triple arrow
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {left:[0x21DA,GENERAL], rep:[0x2261,GENERAL]}
    },
    0x21DB: // right triple arrow
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x21DB,GENERAL], rep:[0x2261,GENERAL]}
    },
    0x23B4: // top square bracket
    {
      dir: H, HW: [[.926,GENERAL],[1.063,SIZE1],[1.606,SIZE2],[2.147,SIZE3],[2.692,SIZE4],[3.237,SIZE5]],
      stretch: {left:[0x2310,GENERAL], rep:[0x2212,GENERAL,0,.12], right:[0xAC,GENERAL]}
    },
    0x23B5: // bottom square bracket
    {
      dir: H, HW: [[.926,GENERAL],[1.063,SIZE1],[1.606,SIZE2],[2.147,SIZE3],[2.692,SIZE4],[3.237,SIZE5]],
      stretch: {left:[0x2A3D,GENERAL,0,.12], rep:[0x2212,GENERAL,0,0,0,.12], right:[0x2A3C,GENERAL,0,.12]}
    },
    0x23DC: // top paren
    {
      dir: H, HW: [[.926,SIZE1],[1,GENERAL],[1.460,SIZE2],[1.886,SIZE3],[2.328,SIZE4],[3.237,SIZE5]],
      stretch: {left:[0xE13B,NONUNI], right:[0xE13C,NONUNI], rep:[0xE14A,NONUNI]}
    },
    0x23DD: // bottom paren
    {
      dir: H, HW: [[.926,SIZE1],[1,GENERAL],[1.460,SIZE2],[1.886,SIZE3],[2.328,SIZE4],[3.237,SIZE5]],
      stretch: {left:[0xE13D,NONUNI], right:[0xE13E,NONUNI], rep:[0xE14B,NONUNI]}
    },
    0x23E0: // top tortoise shell
    {
      dir: H, HW: [[1,GENERAL],[1.460,SIZE1],[1.886,SIZE2],[2.312,SIZE3],[2.738,SIZE4],[3.164,SIZE5]],
      stretch: {left:[0xE10D,NONUNI,-.1,-.1], rep:[0x2212,GENERAL,0,.05], right:[0xE10C,NONUNI,0,-.1], fullExtenders:true}
    },
    0x23E1: // bottom tortoise shell
    {
      dir: H, HW: [[1,GENERAL],[1.460,SIZE1],[1.886,SIZE2],[2.312,SIZE3],[2.738,SIZE4],[3.164,SIZE5]],
      stretch: {left:[0xE10C,NONUNI,-.1,.1], rep:[0x2212,GENERAL,0,-.1,0,.1], right:[0xE10D,NONUNI,0,.1], fullExtenders:true}
    },
    0x2906: // leftwards double arrow from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x21D0,GENERAL], rep:[0x3D,GENERAL], right:[0x2AE4,GENERAL,0,-.09]}
    },
    0x2907: // rightwards double arrow from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x22A8,GENERAL,0,-.09], rep:[0x3D,GENERAL], right:[0x21D2,GENERAL]}
    },
    0x294E: // left barb up right barb up harpoon
    {
      dir: H, HW: [],
      stretch: {left:[0x21BC,GENERAL], rep:[0x2212,GENERAL], right:[0x21C0,GENERAL]}
    },
    0x294F: // up barb right down barb right harpoon
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {top:[0x21BE,GENERAL], ext:[0x23D0,GENERAL], bot:[0x21C2,GENERAL]}
    },
    0x2950: // left barb dow right barb down harpoon
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x21BD,GENERAL], rep:[0x2212,GENERAL], right:[0x21C1,GENERAL]}
    },
    0x2951: // up barb left down barb left harpoon
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {top:[0x21BF,GENERAL], ext:[0x23D0,GENERAL], bot:[0x21C3,GENERAL]}
    },
    0x295A: // leftwards harpoon with barb up from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x21BC,GENERAL], rep:[0x2212,GENERAL], right:[0x22A3,BOLD,0,.1,.6]}
    },
    0x295B: // rightwards harpoon with barb up from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0xE0B6,NONUNI], rep:[0x2212,GENERAL], right:[0x21C0,GENERAL]}
    },
    0x295C: // up harpoon with barb right from bar
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {bot:[0x5F,GENERAL,.05,-.01,.8], ext:[0x23D0,GENERAL], top:[0x21BE,GENERAL]}
    },
    0x295D: // down harpoon with barb right from bar
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {top:[0x22A4,BOLD,0.04,0,.6], ext:[0x23D0,GENERAL], bot:[0x21C2,GENERAL]}
    },
    0x295E: // leftwards harpoon with barb down from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x21BD,GENERAL], rep:[0x2212,GENERAL], right:[0x22A3,BOLD,0,.1,.6]}
    },
    0x295F: // rightwards harpoon with barb down from bar
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0xE0B6,NONUNI], rep:[0x2212,GENERAL], right:[0x21C1,GENERAL]}
    },
    0x2960: // up harpoon with barb left from bar
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {bot:[0x5F,GENERAL,.05,-.01,.8], ext:[0x23D0,GENERAL], top:[0x21BF,GENERAL]}
    },
    0x2961: // down harpoon with barb left from bar
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {top:[0x22A4,BOLD,0.04,0,.6], ext:[0x23D0,GENERAL], bot:[0x21C3,GENERAL]}
    },
    
    0x02C7: // caron
    {
      dir: H, HW: [[.333,GENERAL],[.56,SIZE1],[.979,SIZE2],[1.458,SIZE3],[1.886,SIZE4],[2.328,SIZE5]]
    },
    0x02CD: // low macron
    {
      dir: H, HW: [[.334,GENERAL]], stretch: {rep:[0x2CD,GENERAL]}
    },
    0x02F7: // low tilde
    {
      dir: H, HW: [[.558,SIZE1],[.977,SIZE2],[1.458,SIZE3],[1.886,SIZE4],[2.328,SIZE5]]
    },
    0x219F: // upwards two headed arrow
    {
      dir: V, HW: [[.816,GENERAL]], stretch: {ext:[0x23D0,GENERAL], top:[0x219F,GENERAL]}
    },
    0x21A1: // downwards two headed arrow
    {
      dir: V, HW: [[.816,GENERAL]], stretch: {ext:[0x23D0,GENERAL], bot:[0x21A1,GENERAL]}
    },
    0x21A8: // up down arrow with base
    {
      dir: V, HW: [[.816,GENERAL]],
      stretch: {top:[0x2191,GENERAL], ext:[0x23D0,GENERAL], bot:[0x2913,GENERAL]}
    },
    0x21A9: // left hook arrow
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x2190,GENERAL], rep:[0x2212,GENERAL], right:[0xE0B5,NONUNI]}
    },
    0x21AA: // right hook arrow
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0xE0B4,NONUNI], rep:[0x2212,GENERAL], right:[0x2192,GENERAL]}
    },
    0x21B2: // down arrow with tip left
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x21B2,GENERAL], ext:[0x23D0,GENERAL,.152]}
    },
    0x21B3: // down arrow with tip right
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x21B3,GENERAL], ext:[0x23D0,GENERAL,-.195]}
    },
    0x21B4: // right arrow with corner down
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {rep:[0x2212,GENERAL,0,.4], right:[0x21B4,GENERAL]}
    },
    0x21B5: // down arrow with corner left
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x21B5,GENERAL], ext:[0x23D0,GENERAL,.57]}
    },
    0x21CB: // left harpoon over right harpoon
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x296A,GENERAL], rep:[0x3D,GENERAL], right:[0x296D,GENERAL]}
    },
    0x21CC: // right harpoon over left harpoon
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x296B,GENERAL], rep:[0x3D,GENERAL], right:[0x296C,GENERAL]}
    },
    0x21E0: // left dashed arrow
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x21E0,GENERAL], rep:[0xE121,NONUNI,0,0,0,0,.1], fullExtenders:true}
    },
    0x21E1: // up dashed arrow
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {ext:[0xE12D,NONUNI], top:[0x21E1,GENERAL], fullExtenders: true}
    },
    0x21E2: // right dashed arrow
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {right:[0x21E2,VARIANT], rep:[0xE12E,NONUNI,0,0,0,0,.1], fullExtenders:true}
    },
    0x21E3: // down dashed arrow
    {
      dir: V, HW: [[.818,GENERAL]],
      stretch: {ext:[0xE12C,NONUNI], bot:[0x21E3,GENERAL], fullExtenders: true}
    },
    0x21E4: // left arrow to bar
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {left:[0x21E4,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21E5: // right arrow to bar
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x21E5,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21FD: // left open-headed arrow
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {left:[0x21FD,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21FE: // right open-headed arrow
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x21FE,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x21FF: // left right open-headed arrow
    {
      dir: H, HW: [[.926,GENERAL]],
      stretch: {left:[0x21FD,GENERAL], rep:[0x2212,GENERAL], right:[0x21FE,GENERAL]}
    },
    0x27E6: // left white square bracket
    {
      dir: V, HW: [[.93,GENERAL],[1.23,SIZE1],[1.845,SIZE2],[2.46,SIZE3],[3.075,SIZE4]],
      stretch: {top:[0x2553,GENERAL], ext:[0x2551,GENERAL], bot:[0x2559,GENERAL]}
    },
    0x27E7: // right white square bracket
    {
      dir: V, HW: [[.93,GENERAL],[1.23,SIZE1],[1.845,SIZE2],[2.46,SIZE3],[3.075,SIZE4]],
      stretch: {top:[0x2556,GENERAL], ext:[0x2551,GENERAL], bot:[0x255C,GENERAL]}
    },
    0x27EA: // left double angle bracket
    {
      dir: V, HW: [[.931,GENERAL],[1.23,SIZE1],[1.845,SIZE2],[2.461,SIZE3],[3.075,SIZE4]]
    },
    0x27EB: // right double angle bracket
    {
      dir: V, HW: [[.931,GENERAL],[1.23,SIZE1],[1.845,SIZE2],[2.461,SIZE3],[3.075,SIZE4]]
    },
    0x290A: // up triple arrow
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x290A,GENERAL], ext:[0xE135,NONUNI]}
    },
    0x290B: // down triple arrow
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x290B,GENERAL], ext:[0xE135,NONUNI]}
    },
    0x2912: // up arrow to bar
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x2912,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x2913: // down arrow to bar
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x2913,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x2952: // left harpoon with barb up to bar
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {left:[0x2952,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x2953: // right harpoon with barb up to bar
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x2953,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x2954: // up harpoon with barb right to bar
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x2954,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x2955: // down harpoon with barb right to bar
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x2955,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x2956: // left harpoon with barb down to bar
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {left:[0x2956,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x2957: // right harpoon with barb down to bar
    {
      dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x2957,GENERAL], rep:[0x2212,GENERAL]}
    },
    0x2958: // up harpoon with barb left to bar
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x2958,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x2959: // down harpoon with barb left to bar
    {
      dir: V, HW: [[.818,GENERAL]], stretch: {bot:[0x2959,GENERAL], ext:[0x23D0,GENERAL]}
    },
    0x2980: // triple vertical bar
    {
      dir: V, HW: [[.874,GENERAL]], stretch: {ext:[0x2980,GENERAL]}
    },
    0x2997: // left black tortoise shell
    {
      dir: V, HW: [[.932,GENERAL]],
      stretch: {top:[0xE10D,NONUNI,.1,.05], ext:[0x23D0,GENERAL,-.1], bot:[0xE10C,NONUNI,.1]}
    },
    0x2998: // right black tortoise shell
    {
      dir: V, HW: [[.932,GENERAL]],
      stretch: {top:[0xE10C,NONUNI,-.1,.05], ext:[0x23D0,GENERAL], bot:[0xE10D,NONUNI,-.1]}
    }

  };
  
  for (var id in delim) {if (delim.hasOwnProperty(id)) {DELIMITERS[id] = delim[id]}};

  MathJax.Ajax.loadComplete(HTMLCSS.fontDir + "/fontdata-extra.js");

})(MathJax.OutputJax["HTML-CSS"]);