www

commit 9942283db037dc1e68e2647343a8936d7b9f0693
parent 1846929110a1b7b8561491fe13b64c8e85b97b66
Author: Martin von Gagern <gagern@ma.tum.de>
Date:   Tue,  7 Jul 2015 01:59:11 +0200

Fix incorrect symbol types

These symbols should have different types, according to symgroups.js

Diffstat:
M
src/symbols.js
 | 
30
+++++++++++++++---------------

1 file changed, 15 insertions(+), 15 deletions(-)
diff --git a/src/symbols.js b/src/symbols.js
@@ -920,22 +920,22 @@ var symbols = {
         // AMS Delimiters
         "\\ulcorner": {
             font: "ams",
-            group: "textord",
+            group: "open",
             replace: "\u250c"
         },
         "\\urcorner": {
             font: "ams",
-            group: "textord",
+            group: "close",
             replace: "\u2510"
         },
         "\\llcorner": {
             font: "ams",
-            group: "textord",
+            group: "open",
             replace: "\u2514"
         },
         "\\lrcorner": {
             font: "ams",
-            group: "textord",
+            group: "close",
             replace: "\u2518"
         },
 
@@ -2172,12 +2172,12 @@ var symbols = {
         },
         "\\barwedge": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u22bc"
         },
         "\\veebar": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u22bb"
         },
         "\\odot": {
@@ -2207,12 +2207,12 @@ var symbols = {
         },
         "\\circledcirc": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u229a"
         },
         "\\boxdot": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u22a1"
         },
         "\\bigtriangleup": {
@@ -2327,32 +2327,32 @@ var symbols = {
         },
         "\\uparrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u2191"
         },
         "\\Uparrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u21d1"
         },
         "\\downarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u2193"
         },
         "\\Downarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u21d3"
         },
         "\\updownarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u2195"
         },
         "\\Updownarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u21d5"
         },
         "\\coprod": {
@@ -2447,7 +2447,7 @@ var symbols = {
         },
         "\\ldots": {
             font: "main",
-            group: "punct",
+            group: "inner",
             replace: "\u2026"
         },
         "\\cdots": {