From 79ab06d88dc24d607c970fbe027d5dc27cf283a0 Mon Sep 17 00:00:00 2001
From: Emily Eisenberg <emily@khanacademy.org>
Date: Fri, 12 Sep 2014 17:29:49 -0700
Subject: [PATCH] Get rid of the lookahead-y dots

Summary:
The `\dots` and `\dots{c,o,b,i,m}` commands do more than just show characters,
they add extra space and `\dots` also looks ahead to determine what kind of
environment it is in (see [this math.sx post]
(http://tex.stackexchange.com/questions/122491/difference-of-the-dots)). We
can't support that yet, so remove them.

Also, add comments to the extract_ttf script to show what caracters we are
extracting metrics for.

Test Plan: - Make sure tests work

Reviewers: alpert

Reviewed By: alpert

Differential Revision: http://phabricator.khanacademy.org/D13151
---
 metrics/extract_ttfs.py | 16 ++++++++--------
 symbols.js              | 30 ------------------------------
 2 files changed, 8 insertions(+), 38 deletions(-)

diff --git a/metrics/extract_ttfs.py b/metrics/extract_ttfs.py
index 359ad2927..b9b65fae3 100755
--- a/metrics/extract_ttfs.py
+++ b/metrics/extract_ttfs.py
@@ -6,14 +6,14 @@ import json
 
 metrics_to_extract = {
     "Main-Regular": [
-        u"\u2260",
-        u"\u2245",
-        u"\u0020",
-        u"\u00a0",
-        u"\u2026",
-        u"\u22ef",
-        u"\u22f1",
-        u"\u22ee",
+        u"\u2260",  # \neq
+        u"\u2245",  # \cong
+        u"\u0020",  # space
+        u"\u00a0",  # nbsp
+        u"\u2026",  # \ldots
+        u"\u22ef",  # \cdots
+        u"\u22f1",  # \ddots
+        u"\u22ee",  # \vdots
     ]
 }
 
diff --git a/symbols.js b/symbols.js
index 9ba670268..0ccceb880 100644
--- a/symbols.js
+++ b/symbols.js
@@ -769,41 +769,11 @@ var symbols = {
             group: "punct",
             replace: "\u2026"
         },
-        "\\dotsc": {
-            font: "main",
-            group: "punct",
-            replace: "\u2026"
-        },
-        "\\dotso": {
-            font: "main",
-            group: "punct",
-            replace: "\u2026"
-        },
-        "\\dots": {
-            font: "main",
-            group: "punct",
-            replace: "\u2026"
-        },
         "\\cdots": {
             font: "main",
             group: "punct",
             replace: "\u22ef"
         },
-        "\\dotsb": {
-            font: "main",
-            group: "punct",
-            replace: "\u22ef"
-        },
-        "\\dotsm": {
-            font: "main",
-            group: "punct",
-            replace: "\u22ef"
-        },
-        "\\dotsi": {
-            font: "main",
-            group: "punct",
-            replace: "\u22ef"
-        },
         "\\ddots": {
             font: "main",
             group: "punct",