From cc3fb0c51fa1322a654918dbbb2ab4efb9dd3202 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 12:39:41 -0700 Subject: [PATCH] feat(util/name_generator): allow name generator to be created without providing any argument in the Lua API Signed-off-by: Leonardo de Moura --- src/util/name_generator.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/util/name_generator.cpp b/src/util/name_generator.cpp index 0bfd00cde..eab7d2c78 100644 --- a/src/util/name_generator.cpp +++ b/src/util/name_generator.cpp @@ -26,7 +26,13 @@ void swap(name_generator & a, name_generator & b) { } DECL_UDATA(name_generator) -static int mk_name_generator(lua_State * L) { return push_name_generator(L, name_generator(to_name_ext(L, 1))); } +static name g_tmp_prefix = name::mk_internal_unique_name(); +static int mk_name_generator(lua_State * L) { + if (lua_gettop(L) == 0) + return push_name_generator(L, name_generator(g_tmp_prefix)); + else + return push_name_generator(L, name_generator(to_name_ext(L, 1))); +} static int name_generator_next(lua_State * L) { return push_name(L, to_name_generator(L, 1).next()); } static int name_generator_prefix(lua_State * L) { return push_name(L, to_name_generator(L, 1).prefix()); } static int name_generator_mk_child(lua_State * L) { return push_name_generator(L, to_name_generator(L, 1).mk_child()); }