From 0d42a902ac0679981ef3d43f530ae4f2f3884e3a Mon Sep 17 00:00:00 2001
From: Emily Eisenberg <emily@khanacademy.org>
Date: Sat, 13 Sep 2014 19:04:29 -0700
Subject: [PATCH] Fix dots spacing

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

Test plan:
 - Make sure no huxley tests changed

Auditors: alpert
---
 buildTree.js | 6 ++++++
 symbols.js   | 6 +++---
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/buildTree.js b/buildTree.js
index 4ec6700..297ad1f 100644
--- a/buildTree.js
+++ b/buildTree.js
@@ -30,6 +30,7 @@ var groupToType = {
     text: "mord",
     open: "mopen",
     close: "mclose",
+    inner: "minner",
     frac: "minner",
     spacing: "mord",
     punct: "mpunct",
@@ -243,6 +244,11 @@ var groupTypes = {
             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) {
         var fstyle = options.style;
         if (group.value.size === "dfrac") {
diff --git a/symbols.js b/symbols.js
index 0ccceb8..5c26349 100644
--- a/symbols.js
+++ b/symbols.js
@@ -771,17 +771,17 @@ var symbols = {
         },
         "\\cdots": {
             font: "main",
-            group: "punct",
+            group: "inner",
             replace: "\u22ef"
         },
         "\\ddots": {
             font: "main",
-            group: "punct",
+            group: "inner",
             replace: "\u22f1"
         },
         "\\vdots": {
             font: "main",
-            group: "punct",
+            group: "textord",
             replace: "\u22ee"
         }
     },