feat(library/documentation): add lean suffix to code blocks

src/library/documentation.cpp

@@ -95,10 +95,38 @@ static std::string unindent(std::string const & s) {
     }
 }
 
+static std::string add_lean_suffix_to_code_blocks(std::string const & s) {
+    std::string r;
+    unsigned sz = s.size();
+    unsigned i = 0;
+    bool in_block = false;
+    while (i < sz) {
+        if (!in_block && s[i] == '`' && sz >= 4 && i < sz - 3 && s[i+1] == '`' && s[i+2] == '`' && isspace(s[i+3])) {
+            r += "```lean";
+            r += s[i+3];
+            i += 4;
+            in_block = true;
+        } else if (in_block && s[i] == '`' && sz >= 3 && i < sz - 2 && s[i+1] == '`' && s[i+2] == '`') {
+            r += "```";
+            i += 3;
+            in_block = false;
+        } else {
+            r += s[i];
+            i++;
+        }
+    }
+    if (in_block) {
+        std::cout << "------" << r << "-----\n";
+        throw exception("invalid doc string, end of code block ``` expected");
+    }
+    return r;
+}
+
 static std::string process_doc(std::string s) {
     remove_blank_lines_begin(s);
     rtrim(s);
-    return unindent(s);
+    s = unindent(s);
+    return add_lean_suffix_to_code_blocks(s);
 }
 
 environment add_module_doc_string(environment const & env, std::string doc) {

src/shell/leandoc.cpp

@@ -131,7 +131,7 @@ static void print_inductive(std::ostream & out, environment const & env, formatt
             format r   = format(c);
             r += space() + colon() + space();
             r += nest(get_pp_indent(o), line() + fmt(env.get(c).get_type()));
-            out << mk_pair(r, o) << "\n";
+            out << mk_pair(group(r), o) << "\n";
         }
         out << "```\n";
     }
@@ -181,9 +181,9 @@ void gen_doc(environment const & env, options const & _opts, std::ostream & out)
         if (auto decl_name = entry.get_decl_name()) {
             gen_decl_doc(out, env, fmt, *decl_name);
             out << "\n";
-            out << entry.get_doc() << "\n";
+            out << entry.get_doc();
         } else {
-            out << entry.get_doc() << "\n";
+            out << entry.get_doc();
         }
         out << "\n";
     }