From 7c8ea806388ddc7f771b83ee7877fc6ef7540605 Mon Sep 17 00:00:00 2001
From: Martin von Gagern <gagern@ma.tum.de>
Date: Wed, 8 Jul 2015 23:37:12 +0200
Subject: [PATCH] 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.
---
 src/delimiter.js | 24 +++++++++++++++++++++++-
 src/functions.js |  2 ++
 src/symbols.js   | 10 ++++++++++
 3 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/src/delimiter.js b/src/delimiter.js
index 91e52f212..f94fa9bab 100644
--- 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
index 9b1d2a4ef..6f6a1792b 100644
--- 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
index b620d730f..45590db5c 100644
--- 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"