michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/notation_cmd): relax restriction on user defined tokens

Browse source 
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 ')'.
This commit is contained in:
Leonardo de Moura 2016-01-02 13:58:46 -08:00
parent 4eb2690c32
commit 5feef27c2b
3 changed files with 19 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/algebra/interval.lean
View file

@ -32,14 +32,14 @@ definition Icu (a : A) : set A := {x | a ≤ x}
definition Iuo (b : A) : set A := {x | x < b} definition Iuo (b : A) : set A := {x | x < b}
definition Iuc (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 `)` := Ioo a b
notation `'` `(` a `, ` b `]` := Ioc a b notation `'(` a `, ` b `]` := Ioc a b
notation `'[` a `, ` b `)` := Ico a b notation `'[` a `, ` b `)` := Ico a b
notation `'[` a `, ` b `]` := Icc a b notation `'[` a `, ` b `]` := Icc a b
notation `'` `(` a `, ` `∞` `)` := Iou a notation `'(` a `, ` `∞` `)` := Iou a
notation `'[` a `, ` `∞` `)` := Icu a notation `'[` a `, ` `∞` `)` := Icu a
notation `'` `(` `-∞` `, ` b `)` := Iuo b notation `'(` `-∞` `, ` b `)` := Iuo b
notation `'` `(` `-∞` `, ` b `]` := Iuc b notation `'(` `-∞` `, ` b `]` := Iuc b
variables a b : A variables a b : A

9
src/frontends/lean/notation_cmd.cpp
View file

@ -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); 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) { 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) { while (tk && *tk) {
unsigned sz = get_utf8_size(*tk); unsigned sz = get_utf8_size(*tk);
if (sz == 0) { if (sz == 0) {

6
tests/lean/notation5.lean.expected.out
View file

@ -1,5 +1,5 @@
notation5.lean:3: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 contains reserved character `(` notation5.lean:5:0: error: invalid token `(`, it starts with '('
notation5.lean:7:0: error: invalid token `))`, it contains reserved character `)` notation5.lean:7:0: error: invalid token `))`, it ends with ')'
notation5.lean:9:0: error: invalid token `,,`, it contains reserved character `,` notation5.lean:9:0: error: invalid token `,,`, it contains reserved character `,`
notation5.lean:11:0: error: invalid token `,`, it contains reserved character `,` notation5.lean:11:0: error: invalid token `,`, it contains reserved character `,`