feat(frontends/lean/builtin_cmds): add 'print options' command

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

src/frontends/lean/builtin_cmds.cpp

@@ -26,6 +26,7 @@ static name g_private("[private]");
 static name g_inline("[inline]");
 static name g_true("true");
 static name g_false("false");
+static name g_options("options");
 
 static void check_atomic(name const & n) {
     if (!n.is_atomic())
@@ -270,12 +271,15 @@ environment theorem_cmd(parser & p) {
 
 environment print_cmd(parser & p) {
     if (p.curr() == scanner::token_kind::String) {
-        p.regular_stream() << p.get_str_val() << "\n";
+        p.regular_stream() << p.get_str_val() << endl;
         p.next();
-    } else if (p.curr_is_token(g_raw)) {
+    } else if (p.curr_is_token_or_id(g_raw)) {
         p.next();
         expr e = p.parse_expr();
-        p.regular_stream() << e << "\n";
+        p.regular_stream() << e << endl;
+    } else if (p.curr_is_token_or_id(g_options)) {
+        p.next();
+        p.regular_stream() << p.ios().get_options() << endl;
     } else {
         throw parser_error("invalid print command", p.pos());
     }

src/frontends/lean/token_table.cpp

@@ -58,7 +58,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
-         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0},
+         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]",

tests/lean/run/t10.lean

@@ -1,2 +1,5 @@
 set_option pp.colors true
 set_option pp.unicode false
+print options
+set_option pp.unicode true
+print options