www

commit 7c8ea806388ddc7f771b83ee7877fc6ef7540605
parent a06744e9411a4ae7527bce5f523fb592a5fe8fa6
Author: Martin von Gagern <gagern@ma.tum.de>
Date:   Wed,  8 Jul 2015 23:37:12 +0200

Provide more delimiters

This adds \lgroup, \rgroup, \lmoustache and \rmoustache,
provides \lVert and \rVert with the correct type for each,
and makes \lvert, \rvert, \lVert and \rVert available
through \left...\right.

Diffstat:
M
src/delimiter.js
 | 
24
+++++++++++++++++++++++-
M
src/functions.js
 | 
2
++
M
src/symbols.js
 | 
10
++++++++++

3 files changed, 35 insertions(+), 1 deletion(-)
diff --git a/src/delimiter.js b/src/delimiter.js
@@ -217,6 +217,26 @@ var makeStackedDelim = function(delim, heightTotal, center, options, mode) {
         bottom = "\u23ad";
         repeat = "\u23aa";
         font = "Size4-Regular";
+    } else if (delim === "\\lgroup") {
+        top = "\u23a7";
+        bottom = "\u23a9";
+        repeat = "\u23aa";
+        font = "Size4-Regular";
+    } else if (delim === "\\rgroup") {
+        top = "\u23ab";
+        bottom = "\u23ad";
+        repeat = "\u23aa";
+        font = "Size4-Regular";
+    } else if (delim === "\\lmoustache") {
+        top = "\u23a7";
+        bottom = "\u23ad";
+        repeat = "\u23aa";
+        font = "Size4-Regular";
+    } else if (delim === "\\rmoustache") {
+        top = "\u23ab";
+        bottom = "\u23a9";
+        repeat = "\u23aa";
+        font = "Size4-Regular";
     } else if (delim === "\\surd") {
         top = "\ue001";
         bottom = "\u23b7";
@@ -312,7 +332,9 @@ var stackLargeDelimiters = [
 var stackAlwaysDelimiters = [
     "\\uparrow", "\\downarrow", "\\updownarrow",
     "\\Uparrow", "\\Downarrow", "\\Updownarrow",
-    "|", "\\|", "\\vert", "\\Vert"
+    "|", "\\|", "\\vert", "\\Vert",
+    "\\lvert", "\\rvert", "\\lVert", "\\rVert",
+    "\\lgroup", "\\rgroup", "\\lmoustache", "\\rmoustache"
 ];
 
 // and delimiters that never stack
diff --git a/src/functions.js b/src/functions.js
@@ -205,6 +205,8 @@ var delimiters = [
     "\\{", "\\lbrace", "\\}", "\\rbrace",
     "\\lfloor", "\\rfloor", "\\lceil", "\\rceil",
     "<", ">", "\\langle", "\\rangle",
+    "\\lvert", "\\rvert", "\\lVert", "\\rVert",
+    "\\lgroup", "\\rgroup", "\\lmoustache", "\\rmoustache",
     "/", "\\backslash",
     "|", "\\vert", "\\|", "\\Vert",
     "\\uparrow", "\\Uparrow",
diff --git a/src/symbols.js b/src/symbols.js
@@ -1946,6 +1946,11 @@ var symbols = {
             group: "open",
             replace: "\u2223"
         },
+        "\\lVert": {
+            font: "main",
+            group: "open",
+            replace: "\u2225"
+        },
         ")": {
             font: "main",
             group: "close"
@@ -1972,6 +1977,11 @@ var symbols = {
             group: "close",
             replace: "\u2223"
         },
+        "\\rVert": {
+            font: "main",
+            group: "close",
+            replace: "\u2225"
+        },
         "=": {
             font: "main",
             group: "rel"