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

@@ -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
     ]
 }
 

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",