From 5feef27c2bc92fdc58082329ab9034b564f2ef18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Jan 2016 13:58:46 -0800
Subject: [PATCH] feat(frontends/lean/notation_cmd): relax restriction on user
 defined tokens

Before this commit, Lean would forbid new tokens containing '(' or ')'.
We relax this restriction. Now, we just forbid new tokens starting with '(' or ending with ')'.
---
 library/algebra/interval.lean          | 16 ++++++++--------
 src/frontends/lean/notation_cmd.cpp    |  9 ++++++++-
 tests/lean/notation5.lean.expected.out |  6 +++---
 3 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/library/algebra/interval.lean b/library/algebra/interval.lean
index 98ba3bcad8..c3c4373f7c 100644
--- a/library/algebra/interval.lean
+++ b/library/algebra/interval.lean
@@ -32,14 +32,14 @@ definition Icu (a : A)   : set A := {x | a ≤ x}
 definition Iuo (b : A)   : set A := {x | x < b}
 definition Iuc (b : A)   : set A := {x | x ≤ b}
 
-notation `'` `(` a `, ` b `)`     := Ioo a b
-notation `'` `(` a `, ` b `]`     := Ioc a b
-notation `'[` a `, ` b `)`        := Ico a b
-notation `'[` a `, ` b `]`       := Icc a b
-notation `'` `(` a `, ` `∞` `)`   := Iou a
-notation `'[` a `, ` `∞` `)`      := Icu a
-notation `'` `(` `-∞` `, ` b `)`  := Iuo b
-notation `'` `(` `-∞` `, ` b `]`  := Iuc b
+notation `'(` a `, ` b `)`     := Ioo a b
+notation `'(` a `, ` b `]`     := Ioc a b
+notation `'[` a `, ` b `)`     := Ico a b
+notation `'[` a `, ` b `]`     := Icc a b
+notation `'(` a `, ` `∞` `)`   := Iou a
+notation `'[` a `, ` `∞` `)`   := Icu a
+notation `'(` `-∞` `, ` b `)`  := Iuo b
+notation `'(` `-∞` `, ` b `]`  := Iuc b
 
 variables a b : A
 
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index c6770b0f68..b193cc4485 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -662,9 +662,16 @@ notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & n
     return parse_notation(p, overload, grp, new_tokens, allow_local);
 }
 
-static char g_reserved_chars[] = {'(', ')', ',', 0};
+static char g_reserved_chars[] = {',', 0};
 
 static void check_token(char const * tk) {
+    if (!tk || !*tk)
+        throw exception("invalid null token");
+    if (tk[0] == '(')
+        throw exception(sstream() << "invalid token `" << tk << "`, it starts with '('");
+    unsigned sz = strlen(tk);
+    if (tk[sz-1] == ')')
+        throw exception(sstream() << "invalid token `" << tk << "`, it ends with ')'");
     while (tk && *tk) {
         unsigned sz = get_utf8_size(*tk);
         if (sz == 0) {
diff --git a/tests/lean/notation5.lean.expected.out b/tests/lean/notation5.lean.expected.out
index 9234397c57..b695d7e755 100644
--- a/tests/lean/notation5.lean.expected.out
+++ b/tests/lean/notation5.lean.expected.out
@@ -1,5 +1,5 @@
-notation5.lean:3:0: error: invalid token `((`, it contains reserved character `(`
-notation5.lean:5:0: error: invalid token `(`, it contains reserved character `(`
-notation5.lean:7:0: error: invalid token `))`, it contains reserved character `)`
+notation5.lean:3:0: error: invalid token `((`, it starts with '('
+notation5.lean:5:0: error: invalid token `(`, it starts with '('
+notation5.lean:7:0: error: invalid token `))`, it ends with ')'
 notation5.lean:9:0: error: invalid token `,,`, it contains reserved character `,`
 notation5.lean:11:0: error: invalid token `,`, it contains reserved character `,`