From f1462dc51e6a66c18d057a0e503433baa4bd3ead Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Aug 2013 10:55:55 -0700
Subject: [PATCH] Change lean frontend specific options. Now, frontend specific
 options must begin with the frontend name.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/ex11.lean                   |  4 ++--
 src/frontends/lean/lean_pp.cpp       | 12 ++++++------
 src/tests/frontends/lean/lean_pp.cpp |  8 ++++----
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/examples/ex11.lean b/examples/ex11.lean
index a37343a40..da2bab733 100644
--- a/examples/ex11.lean
+++ b/examples/ex11.lean
@@ -2,11 +2,11 @@ Show Options
 Variable a : Bool
 Variable b : Bool
 Show a/\b
-Set pp::lean::notation false
+Set lean::pp::notation false
 Show Options
 Show a/\b
 Show Environment 5
-Set pp::lean::notation true
+Set lean::pp::notation true
 Show Options
 Show a/\b
 
diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp
index f87adf7bb..1f432c7a9 100644
--- a/src/frontends/lean/lean_pp.cpp
+++ b/src/frontends/lean/lean_pp.cpp
@@ -63,12 +63,12 @@ static format g_in_fmt        = highlight_keyword(format("in"));
 static format g_assign_fmt    = highlight_keyword(format(":="));
 static format g_geq_fmt       = format("\u2265");
 
-static name g_pp_max_depth       {"pp", "lean", "max_depth"};
-static name g_pp_max_steps       {"pp", "lean", "max_steps"};
-static name g_pp_implicit        {"pp", "lean", "implicit"};
-static name g_pp_notation        {"pp", "lean", "notation"};
-static name g_pp_extra_lets      {"pp", "lean", "extra_lets"};
-static name g_pp_alias_min_weight{"pp", "lean", "alias_min_weight"};
+static name g_pp_max_depth       {"lean", "pp", "max_depth"};
+static name g_pp_max_steps       {"lean", "pp", "max_steps"};
+static name g_pp_implicit        {"lean", "pp", "implicit"};
+static name g_pp_notation        {"lean", "pp", "notation"};
+static name g_pp_extra_lets      {"lean", "pp", "extra_lets"};
+static name g_pp_alias_min_weight{"lean", "pp", "alias_min_weight"};
 
 RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(lean pretty printer) maximum expression depth, after that it will use ellipsis");
 RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis");
diff --git a/src/tests/frontends/lean/lean_pp.cpp b/src/tests/frontends/lean/lean_pp.cpp
index c7b388be8..eceaae8cf 100644
--- a/src/tests/frontends/lean/lean_pp.cpp
+++ b/src/tests/frontends/lean/lean_pp.cpp
@@ -38,7 +38,7 @@ static void tst2() {
     expr g = Const("g");
     std::cout << fmt(g(t, t, t)) << std::endl;
     formatter fmt2 = mk_pp_formatter(f);
-    std::cout << fmt2(g(t, t, t), options({"pp", "lean", "alias_min_weight"}, 100)) << std::endl;
+    std::cout << fmt2(g(t, t, t), options({"lean", "pp", "alias_min_weight"}, 100)) << std::endl;
 }
 
 static void tst3() {
@@ -64,7 +64,7 @@ static void tst4() {
     regular(s1) << And(Const("a"), Const("b")) << "\n";
     regular(f) << And(Const("a"), Const("b")) << "\n";
     diagnostic(f) << And(Const("a"), Const("b")) << "\n";
-    f.set_option(name{"pp", "lean", "notation"}, false);
+    f.set_option(name{"lean", "pp", "notation"}, false);
     regular(f) << And(Const("a"), Const("b")) << "\n";
     regular(s1) << And(Const("a"), Const("b")) << "\n";
     regular(s2) << And(Const("a"), Const("b")) << "\n";
@@ -76,7 +76,7 @@ static void tst5() {
     f.set_regular_channel(out);
     regular(f) << And(Const("a"), Const("b"));
     lean_assert(out->str() == "a ∧ b");
-    f.set_option(name{"pp", "lean", "notation"}, false);
+    f.set_option(name{"lean", "pp", "notation"}, false);
     regular(f) << " " << And(Const("a"), Const("b"));
     lean_assert(out->str() == "a ∧ b and a b");
 }
@@ -93,7 +93,7 @@ static void tst6() {
     std::shared_ptr<string_output_channel> out(new string_output_channel());
     f.set_regular_channel(out);
     expr t = mk_deep(10);
-    f.set_option(name{"pp", "lean", "max_depth"}, 5);
+    f.set_option(name{"lean", "pp", "max_depth"}, 5);
     f.set_option(name{"pp", "colors"}, false);
     regular(f) << t;
     lean_assert(out->str() == "f (f (f (f (f (…)))))");