From 639d58f4c79e967dc77c011aedef18b761ca8295 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jun 2014 17:31:28 -0700
Subject: [PATCH] feat(frontends/lean/builtin_cmds): add 'print options'
 command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_cmds.cpp | 10 +++++++---
 src/frontends/lean/token_table.cpp  |  2 +-
 tests/lean/run/t10.lean             |  3 +++
 3 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 4e29be7503..fdf500bf86 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/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());
     }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 94c668dd48..acb493a006 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/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]",
diff --git a/tests/lean/run/t10.lean b/tests/lean/run/t10.lean
index c0ede26bdb..a215347ae6 100644
--- a/tests/lean/run/t10.lean
+++ b/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
\ No newline at end of file