diff --git a/MJLite.js b/MJLite.js index 98e8b5f9d..ce47af771 100644 --- a/MJLite.js +++ b/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) { diff --git a/lexer.js b/lexer.js index eb9a14cf0..71f8b91a8 100644 --- a/lexer.js +++ b/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 diff --git a/parser.jison b/parser.jison index db9a1f6bb..0c14f24f4 100644 --- a/parser.jison +++ b/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' diff --git a/static/mjlite.css b/static/mjlite.css index 486d140c7..52ecc5616 100644 --- a/static/mjlite.css +++ b/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%;