From 037cfcf62240582e1502952982ed9e9358014a9f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Jun 2014 13:39:44 -0700 Subject: [PATCH] refactor(frontends/lean/notation_cmd): add register_notation_cmds procedure Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 7 +------ src/frontends/lean/notation_cmd.cpp | 14 ++++++++++++++ src/frontends/lean/notation_cmd.h | 7 +++---- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 39343ca86..c389c1429 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -511,13 +511,8 @@ cmd_table init_cmd_table() { add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd)); add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); - add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd)); - add_cmd(r, cmd_info("infixl", "declare a new infix (left) notation", infixl_cmd)); - add_cmd(r, cmd_info("infix", "declare a new infix (left) notation", infixl_cmd)); - add_cmd(r, cmd_info("infixr", "declare a new infix (right) notation", infixr_cmd)); - add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd)); - add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd)); add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd)); + register_notation_cmds(r); register_calc_cmds(r); return r; } diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 6c695225e..dfaa18bcc 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -297,4 +297,18 @@ notation_entry parse_notation(parser & p, bool overload, buffer & n throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'postfix' or 'notation' expected", p.pos()); } } + +environment notation_cmd(parser & p) { return notation_cmd_core(p, true); } +environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); } +environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); } +environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); } + +void register_notation_cmds(cmd_table & r) { + add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd)); + add_cmd(r, cmd_info("infixl", "declare a new infix (left) notation", infixl_cmd)); + add_cmd(r, cmd_info("infix", "declare a new infix (left) notation", infixl_cmd)); + add_cmd(r, cmd_info("infixr", "declare a new infix (right) notation", infixr_cmd)); + add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd)); + add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd)); +} } diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h index 7f004107d..e12d83c08 100644 --- a/src/frontends/lean/notation_cmd.h +++ b/src/frontends/lean/notation_cmd.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include "kernel/environment.h" #include "frontends/lean/parser_config.h" +#include "frontends/lean/cmd_table.h" namespace lean { class parser; @@ -15,13 +16,11 @@ environment notation_cmd_core(parser & p, bool overload); environment infixl_cmd_core(parser & p, bool overload); environment infixr_cmd_core(parser & p, bool overload); environment postfix_cmd_core(parser & p, bool overload); -inline environment notation_cmd(parser & p) { return notation_cmd_core(p, true); } -inline environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); } -inline environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); } -inline environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); } /** \brief Return true iff the current token is a notation declaration */ bool curr_is_notation_decl(parser & p); /** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */ notation_entry parse_notation(parser & p, bool overload, buffer & new_tokens); + +void register_notation_cmds(cmd_table & r); }