Add punctuation

Summary: Add punctuation, like ",", ";", and "\colon"

Reviewers: spicyj

Reviewed By: spicyj

Differential Revision: http://phabricator.benalpert.com/D49

MJLite.js

@@ -86,6 +86,8 @@ var buildGroup = function(group, prev) {
     } else if (group.type === "rlap") {
         var inner = makeSpan("", buildExpression(group.value));
         return makeSpan("rlap", inner);
+    } else if (group.type === "punct") {
+        return makeSpan("mpunct", textit(group.value));
     } else {
         console.log("Unknown type:", group.type);
     }
@@ -105,7 +107,8 @@ var charLookup = {
     "\\nleq": "\u2270",
     "\\ngeq": "\u2271",
     "\\ ": "\u00a0",
-    "\\space": "\u00a0"
+    "\\space": "\u00a0",
+    "\\colon": ":"
 };
 
 var textit = function(value) {

lexer.js

@@ -5,6 +5,7 @@ var normals = [
     [/^[/|a-zA-Z0-9.]/, 'ORD'],
     [/^[*+-]/, 'BIN'],
     [/^[=<>]/, 'REL'],
+    [/^[,;]/, 'PUNCT'],
     [/^\^/, '^'],
     [/^_/, '_'],
     [/^{/, '{'],
@@ -20,6 +21,8 @@ var funcs = [
     'leq', 'geq', 'neq', 'nleq', 'ngeq',
     // Open/close symbols
     'lvert', 'rvert',
+    // Punct symbols
+    'colon',
     // Spacing symbols
     'qquad', 'quad', ' ', 'space', ',', ':', ';',
     // Colors

parser.jison

@@ -74,6 +74,8 @@ func
         {$$ = [{type: 'spacing', value: yytext}];}
     | ';'
         {$$ = [{type: 'spacing', value: yytext}];}
+    | 'colon'
+        {$$ = [{type: 'punct', value: yytext}];}
     | 'blue' group
         {$$ = [{type: 'color', value: {color: 'blue', value: $2}}];}
     | 'orange' group
@@ -103,6 +105,8 @@ atom
         {$$ = [{type: 'bin', value: yytext}];}
     | 'REL'
         {$$ = [{type: 'rel', value: yytext}];}
+    | 'PUNCT'
+        {$$ = [{type: 'punct', value: yytext}];}
     | 'OPEN'
         {$$ = [{type: 'open', value: yytext}];}
     | 'CLOSE'

static/mjlite.css

@@ -56,6 +56,30 @@ big parens
     margin-left: 0.27778em;
 }
 
+.mpunct + .mord {
+    margin-left: 0.16667em;
+}
+
+.mpunct + .mbin {
+    margin-left: 0.16667em;
+}
+
+.mpunct + .mrel {
+    margin-left: 0.16667em;
+}
+
+.mpunct + .mopen {
+    margin-left: 0.16667em;
+}
+
+.mpunct + .mclose {
+    margin-left: 0.16667em;
+}
+
+.mpunct + .mpunct {
+    margin-left: 0.16667em;
+}
+
 .msub {
     vertical-align: bottom;
     font-size: 70%;