refactor(frontends/lean/cmd_table): remove register_builtin_cmd procedures, they would cause initialization problems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(lean_frontend register_module.cpp token_table.cpp
-scanner.cpp parse_table.cpp cmd_table.cpp parser_config.cpp parser.cpp
+scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
-parser_pos_provider.cpp)
+parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_cmds.cpp

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "frontends/lean/parser.h"
+
+namespace lean {
+cmd_table get_builtin_cmds() {
+    return cmd_table();
+}
+}
+

src/frontends/lean/builtin_cmds.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "frontends/lean/cmd_table.h"
+namespace lean {
+cmd_table get_builtin_cmds();
+}

src/frontends/lean/builtin_tactic_cmds.cpp

@@ -4,16 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontends/lean/cmd_table.h"
+#include "frontends/lean/parser.h"
 
 namespace lean {
-cmd_table get_builtin_cmds() {
-    // TODO(Leo)
-    return cmd_table();
-}
-
 tactic_cmd_table get_builtin_tactic_cmds() {
-    // TODO(Leo)
     return tactic_cmd_table();
 }
 }

src/frontends/lean/builtin_tactic_cmds.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "frontends/lean/cmd_table.h"
+namespace lean {
+tactic_cmd_table get_builtin_tactic_cmds();
+}

src/frontends/lean/cmd_table.h

@@ -11,24 +11,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 class tactic {};  // TODO(Leo): remove after tactic framework is ported to Lean 0.2
-
 class parser;
 
 typedef std::function<environment(parser&)> command_fn;
-void register_builtin_cmd(char const * name, char const * descr, command_fn const & fn);
-
 typedef std::function<tactic(parser&)> tactic_command_fn;
-void register_builtin_cmd(char const * name, char const * descr, tactic_command_fn const & fn);
-
-template<typename F>
-struct register_builtin_cmd_tmpl {
-    register_builtin_cmd_tmpl(char const * name, char const * descr, F const & fn) {
-        register_builtin_cmd(name, descr, fn);
-    }
-};
-
-typedef register_builtin_cmd_tmpl<command_fn>        register_builtin_cmd_fn;
-typedef register_builtin_cmd_tmpl<tactic_command_fn> register_builtin_tactic_fn;
 
 template<typename F>
 struct cmd_info_tmpl {
@@ -49,7 +35,4 @@ typedef cmd_info_tmpl<tactic_command_fn> tactic_cmd_info;
 
 typedef rb_map<name, cmd_info,        name_quick_cmp> cmd_table;
 typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table;
-
-cmd_table        get_builtin_cmds();
-tactic_cmd_table get_builtin_tactic_cmds();
 }

src/frontends/lean/parser_config.cpp

@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "frontends/lean/parser_config.h"
+#include "frontends/lean/builtin_cmds.h"
+#include "frontends/lean/builtin_tactic_cmds.h"
 
 namespace lean {
 parser_config::parser_config() {