Fix dots spacing

\cdots, \ddots, and \vdots are all ords, not puncts.

Test plan:
 - Make sure no huxley tests changed

Auditors: alpert
This commit is contained in:
Emily Eisenberg 2014-09-13 19:04:29 -07:00
parent 90573fcaf2
commit 0d42a902ac
2 changed files with 9 additions and 3 deletions

View File

@ -30,6 +30,7 @@ var groupToType = {
text: "mord", text: "mord",
open: "mopen", open: "mopen",
close: "mclose", close: "mclose",
inner: "minner",
frac: "minner", frac: "minner",
spacing: "mord", spacing: "mord",
punct: "mpunct", punct: "mpunct",
@ -243,6 +244,11 @@ var groupTypes = {
group.value, group.mode, options.getColor(), ["mclose"]); group.value, group.mode, options.getColor(), ["mclose"]);
}, },
inner: function(group, options, prev) {
return buildCommon.mathrm(
group.value, group.mode, options.getColor(), ["minner"]);
},
frac: function(group, options, prev) { frac: function(group, options, prev) {
var fstyle = options.style; var fstyle = options.style;
if (group.value.size === "dfrac") { if (group.value.size === "dfrac") {

View File

@ -771,17 +771,17 @@ var symbols = {
}, },
"\\cdots": { "\\cdots": {
font: "main", font: "main",
group: "punct", group: "inner",
replace: "\u22ef" replace: "\u22ef"
}, },
"\\ddots": { "\\ddots": {
font: "main", font: "main",
group: "punct", group: "inner",
replace: "\u22f1" replace: "\u22f1"
}, },
"\\vdots": { "\\vdots": {
font: "main", font: "main",
group: "punct", group: "textord",
replace: "\u22ee" replace: "\u22ee"
} }
}, },